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