Theorem fvsingle

Description: The value of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Revised by Scott Fenton, 13-Apr-2018)

	Ref	Expression
Assertion	fvsingle	⊢ ( Singleton ‘ 𝐴 ) = { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐴 → ( Singleton ‘ 𝑥 ) = ( Singleton ‘ 𝐴 ) )
2		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
3	1 2	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( Singleton ‘ 𝑥 ) = { 𝑥 } ↔ ( Singleton ‘ 𝐴 ) = { 𝐴 } ) )
4		eqid	⊢ { 𝑥 } = { 𝑥 }
5		vex	⊢ 𝑥 ∈ V
6		vsnex	⊢ { 𝑥 } ∈ V
7	5 6	brsingle	⊢ ( 𝑥 Singleton { 𝑥 } ↔ { 𝑥 } = { 𝑥 } )
8	4 7	mpbir	⊢ 𝑥 Singleton { 𝑥 }
9		fnsingle	⊢ Singleton Fn V
10		fnbrfvb	⊢ ( ( Singleton Fn V ∧ 𝑥 ∈ V ) → ( ( Singleton ‘ 𝑥 ) = { 𝑥 } ↔ 𝑥 Singleton { 𝑥 } ) )
11	9 5 10	mp2an	⊢ ( ( Singleton ‘ 𝑥 ) = { 𝑥 } ↔ 𝑥 Singleton { 𝑥 } )
12	8 11	mpbir	⊢ ( Singleton ‘ 𝑥 ) = { 𝑥 }
13	3 12	vtoclg	⊢ ( 𝐴 ∈ V → ( Singleton ‘ 𝐴 ) = { 𝐴 } )
14		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( Singleton ‘ 𝐴 ) = ∅ )
15		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
16	15	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
17	14 16	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → ( Singleton ‘ 𝐴 ) = { 𝐴 } )
18	13 17	pm2.61i	⊢ ( Singleton ‘ 𝐴 ) = { 𝐴 }