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

Metamath Proof Explorer

Theorem fsn2g

Description: A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by Thierry Arnoux, 11-Jul-2020)

Ref Expression
Assertion fsn2g ⊢ A ∈ V → F : A ⟶ B ↔ F ⁡ A ∈ B ∧ F = A F ⁡ A

Proof

Step Hyp Ref Expression
1 sneq ⊢ a = A → a = A
2 1 feq2d ⊢ a = A → F : a ⟶ B ↔ F : A ⟶ B
3 fveq2 ⊢ a = A → F ⁡ a = F ⁡ A
4 3 eleq1d ⊢ a = A → F ⁡ a ∈ B ↔ F ⁡ A ∈ B
5 id ⊢ a = A → a = A
6 5 3 opeq12d ⊢ a = A → a F ⁡ a = A F ⁡ A
7 6 sneqd ⊢ a = A → a F ⁡ a = A F ⁡ A
8 7 eqeq2d ⊢ a = A → F = a F ⁡ a ↔ F = A F ⁡ A
9 4 8 anbi12d ⊢ a = A → F ⁡ a ∈ B ∧ F = a F ⁡ a ↔ F ⁡ A ∈ B ∧ F = A F ⁡ A
10 vex ⊢ a ∈ V
11 10 fsn2 ⊢ F : a ⟶ B ↔ F ⁡ a ∈ B ∧ F = a F ⁡ a
12 2 9 11 vtoclbg ⊢ A ∈ V → F : A ⟶ B ↔ F ⁡ A ∈ B ∧ F = A F ⁡ A