Metamath Proof Explorer


Theorem dff12

Description: Alternate definition of a one-to-one function. (Contributed by NM, 31-Dec-1996)

Ref Expression
Assertion dff12 ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ) )

Proof

Step Hyp Ref Expression
1 df-f1 ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ Fun 𝐹 ) )
2 funcnv2 ( Fun 𝐹 ↔ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 )
3 2 anbi2i ( ( 𝐹 : 𝐴𝐵 ∧ Fun 𝐹 ) ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ) )
4 1 3 bitri ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ) )