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 ` A ) = { A }

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( x = A -> ( Singleton ` x ) = ( Singleton ` A ) )
2		sneq	|- ( x = A -> { x } = { A } )
3	1 2	eqeq12d	|- ( x = A -> ( ( Singleton ` x ) = { x } <-> ( Singleton ` A ) = { A } ) )
4		eqid	|- { x } = { x }
5		vex	|- x e. _V
6		snex	|- { x } e. _V
7	5 6	brsingle	|- ( x Singleton { x } <-> { x } = { x } )
8	4 7	mpbir	|- x Singleton { x }
9		fnsingle	|- Singleton Fn _V
10		fnbrfvb	|- ( ( Singleton Fn _V /\ x e. _V ) -> ( ( Singleton ` x ) = { x } <-> x Singleton { x } ) )
11	9 5 10	mp2an	|- ( ( Singleton ` x ) = { x } <-> x Singleton { x } )
12	8 11	mpbir	|- ( Singleton ` x ) = { x }
13	3 12	vtoclg	|- ( A e. _V -> ( Singleton ` A ) = { A } )
14		fvprc	|- ( -. A e. _V -> ( Singleton ` A ) = (/) )
15		snprc	|- ( -. A e. _V <-> { A } = (/) )
16	15	biimpi	|- ( -. A e. _V -> { A } = (/) )
17	14 16	eqtr4d	|- ( -. A e. _V -> ( Singleton ` A ) = { A } )
18	13 17	pm2.61i	|- ( Singleton ` A ) = { A }