关于多对一函数的谓词逻辑表示及验证方法的技术问询

我最近在学习离散数学，尝试用命题演算或谓词演算的形式来描述数学定义和定理，但不确定自己的思路是否正确。

举个例子，多对一函数的定义是：定义域中存在两个不同的元素，它们映射到值域中的同一个元素。

我是这样尝试描述的：
设 $ f : A \to B $ 是一个函数，定义命题 $ P $ 为：
$$ P \equiv(f \text{ 是一个多对一函数})\iff (\exists x, y \in A, (x \ne y) \implies (f(x) = f(y))) $$

为了确保这个命题的正确性，我想到了用真值表验证的方法：
假设
$$ P \equiv T $$
且
$$ (f \text{ 是一个多对一函数}) \equiv T $$
那么
$$ \exists x, y \in A, (x \ne y) \implies (f(x) = f(y)) \equiv T $$
接着……

备注：内容来源于stack exchange，提问作者咪苦力怕