Theorem elsingles

Description: Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)

	Ref	Expression
Assertion	elsingles	|- ( A e. Singletons <-> E. x A = { x } )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. Singletons -> A e. _V )
2		snex	|- { x } e. _V
3		eleq1	|- ( A = { x } -> ( A e. _V <-> { x } e. _V ) )
4	2 3	mpbiri	|- ( A = { x } -> A e. _V )
5	4	exlimiv	|- ( E. x A = { x } -> A e. _V )
6		eleq1	|- ( y = A -> ( y e. Singletons <-> A e. Singletons ) )
7		eqeq1	|- ( y = A -> ( y = { x } <-> A = { x } ) )
8	7	exbidv	|- ( y = A -> ( E. x y = { x } <-> E. x A = { x } ) )
9		df-singles	|- Singletons = ran Singleton
10	9	eleq2i	|- ( y e. Singletons <-> y e. ran Singleton )
11		vex	|- y e. _V
12	11	elrn	|- ( y e. ran Singleton <-> E. x x Singleton y )
13		vex	|- x e. _V
14	13 11	brsingle	|- ( x Singleton y <-> y = { x } )
15	14	exbii	|- ( E. x x Singleton y <-> E. x y = { x } )
16	10 12 15	3bitri	|- ( y e. Singletons <-> E. x y = { x } )
17	6 8 16	vtoclbg	|- ( A e. _V -> ( A e. Singletons <-> E. x A = { x } ) )
18	1 5 17	pm5.21nii	|- ( A e. Singletons <-> E. x A = { x } )