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 ( 𝐴 ∈ 𝑉 → ( 𝐹 : { 𝐴 } ⟶ 𝐵 ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) ) )

Proof

Step Hyp Ref Expression
1 sneq ⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
2 1 feq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐹 : { 𝑎 } ⟶ 𝐵 ↔ 𝐹 : { 𝐴 } ⟶ 𝐵 ) )
3 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐴 ) )
4 3 eleq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 ↔ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
5 id ⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
6 5 3 opeq12d ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ )
7 6 sneqd ⊢ ( 𝑎 = 𝐴 → { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
8 7 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )
9 4 8 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) ) )
10 vex ⊢ 𝑎 ∈ V
11 10 fsn2 ⊢ ( 𝐹 : { 𝑎 } ⟶ 𝐵 ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝑎 , ( 𝐹 ‘ 𝑎 ) ⟩ } ) )
12 2 9 11 vtoclbg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : { 𝐴 } ⟶ 𝐵 ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) ) )