This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dff12

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

Ref Expression
Assertion dff12 ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ ∀ y ∃* x x F y

Proof

Step Hyp Ref Expression
1 df-f1 ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ Fun ⁡ F -1
2 funcnv2 ⊢ Fun ⁡ F -1 ↔ ∀ y ∃* x x F y
3 2 anbi2i ⊢ F : A ⟶ B ∧ Fun ⁡ F -1 ↔ F : A ⟶ B ∧ ∀ y ∃* x x F y
4 1 3 bitri ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ ∀ y ∃* x x F y