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

Proof

Step Hyp Ref Expression
1 sneq ⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
2 1 feq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐹 : { 𝑎 } ⟶ { 𝑏 } ↔ 𝐹 : { 𝐴 } ⟶ { 𝑏 } ) )
3 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
4 3 sneqd ⊢ ( 𝑎 = 𝐴 → { ⟨ 𝑎 , 𝑏 ⟩ } = { ⟨ 𝐴 , 𝑏 ⟩ } )
5 4 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , 𝑏 ⟩ } ) )
6 2 5 bibi12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 : { 𝑎 } ⟶ { 𝑏 } ↔ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ } ) ↔ ( 𝐹 : { 𝐴 } ⟶ { 𝑏 } ↔ 𝐹 = { ⟨ 𝐴 , 𝑏 ⟩ } ) ) )
7 sneq ⊢ ( 𝑏 = 𝐵 → { 𝑏 } = { 𝐵 } )
8 7 feq3d ⊢ ( 𝑏 = 𝐵 → ( 𝐹 : { 𝐴 } ⟶ { 𝑏 } ↔ 𝐹 : { 𝐴 } ⟶ { 𝐵 } ) )
9 opeq2 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
10 9 sneqd ⊢ ( 𝑏 = 𝐵 → { ⟨ 𝐴 , 𝑏 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ } )
11 10 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐹 = { ⟨ 𝐴 , 𝑏 ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } ) )
12 8 11 bibi12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 : { 𝐴 } ⟶ { 𝑏 } ↔ 𝐹 = { ⟨ 𝐴 , 𝑏 ⟩ } ) ↔ ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } ) ) )
13 vex ⊢ 𝑎 ∈ V
14 vex ⊢ 𝑏 ∈ V
15 13 14 fsn ⊢ ( 𝐹 : { 𝑎 } ⟶ { 𝑏 } ↔ 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ } )
16 6 12 15 vtocl2g ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐹 : { 𝐴 } ⟶ { 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , 𝐵 ⟩ } ) )