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