Definition 1.5.16.  Let X, Y be sets, f : X → Y be a function. We define:
f is injective  :⇔  ∀ a, b ∈ X s.t. f(a) = f(b) : a = b  ⇔  ∀ c ∈ Y, d, e ∈ f-1({c}) : d = e  ⇔  ∀ y ∈ f(X) : ∃! x ∈ X : f(x) = y  ⇔  X is empty or ∃ g : Y → X : g ∘ f = idX
Equivalence.  No proof.
References.