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

Metamath Proof Explorer

Theorem fsng

Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012)

Ref Expression
Assertion fsng ⊢ A ∈ C ∧ B ∈ D → F : A ⟶ B ↔ F = A B

Proof

Step Hyp Ref Expression
1 sneq ⊢ a = A → a = A
2 1 feq2d ⊢ a = A → F : a ⟶ b ↔ F : A ⟶ b
3 opeq1 ⊢ a = A → a b = A b
4 3 sneqd ⊢ a = A → a b = A b
5 4 eqeq2d ⊢ a = A → F = a b ↔ F = A b
6 2 5 bibi12d ⊢ a = A → F : a ⟶ b ↔ F = a b ↔ F : A ⟶ b ↔ F = A b
7 sneq ⊢ b = B → b = B
8 7 feq3d ⊢ b = B → F : A ⟶ b ↔ F : A ⟶ B
9 opeq2 ⊢ b = B → A b = A B
10 9 sneqd ⊢ b = B → A b = A B
11 10 eqeq2d ⊢ b = B → F = A b ↔ F = A B
12 8 11 bibi12d ⊢ b = B → F : A ⟶ b ↔ F = A b ↔ F : A ⟶ B ↔ F = A B
13 vex ⊢ a ∈ V
14 vex ⊢ b ∈ V
15 13 14 fsn ⊢ F : a ⟶ b ↔ F = a b
16 6 12 15 vtocl2g ⊢ A ∈ C ∧ B ∈ D → F : A ⟶ B ↔ F = A B