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