# Why is this definition of an injective function incorrect?

Consider the following definition: $$\mathrm{function\ } f(x) \mathrm{\ is \ injective} \iff \forall_{a \in D_f} \forall_{b \in D_f} \left( a \neq b \land f(a) \neq f(b) \right)$$

Seems sound to me. But, if we negate it, we get this nonesense: $$\mathrm{function\ } f(x) \mathrm{\ is \ not \ injective } \iff \exists_{a \in D_f} \exists_{b \in D_f} \left( a = b \lor f(a) = f(b) \right)$$

We can conclude that this definition is rubbish. However, this isn't evident at a glance, I cannot see that this definition is invalid without performing the negation trick. Could anyone explain this to me?

$$\forall_{a \in D_f} \forall_{b \in D_f} \left( a \neq b \land f(a) \neq f(b) \right)$$ implies that $$\forall_{a \in D_f} \forall_{b \in D_f} \left( a \neq b\right),$$ i.e. if you take any $$a,b\in D_f$$ then these are different. But when you take $$a$$ you don't remove it from $$D_f$$; it's still there, so $$b$$ can be the same element. Then $$a \neq b$$ is absurd.
Actually, the first definition should be$$f\text{ injective}\iff(\forall a\in D_f)(\exists b\in D_f):a\ne b\implies f(a)\ne f(b).$$Its negation is$$f\text{ not injective}\iff(\exists a\in D_f)(\exists b\in D_f):a\ne b\wedge f(a)=f(b)$$and that makes sense.
The condition should be $$\forall_{a\in D_f}\,\forall_{b\in D_f}(a\ne b\to f(a)\ne f(b))$$ which is very different from the one stated in your question.
You need to express the condition “if $$a\ne b$$, then $$f(a)\ne f(b)$$”. It's a common error to state this improperly as “$$a\ne b$$ and $$f(a)\ne f(b)$$”, but as you see from the negation it is nonsense.
By the way, the statement with $$(a\ne b\land f(a)\ne f(b))$$ is false unless the domain of $$f$$ is empty.