Theorem bj-snglex

Description: A class is a set if and only if its singletonization is a set. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-snglex	|- ( A e. _V <-> sngl A e. _V )

Proof

Step	Hyp	Ref	Expression
1		isset	|- ( A e. _V <-> E. x x = A )
2		pweq	|- ( x = A -> ~P x = ~P A )
3	2	eximi	|- ( E. x x = A -> E. x ~P x = ~P A )
4		bj-snglss	|- sngl A C_ ~P A
5		sseq2	|- ( ~P x = ~P A -> ( sngl A C_ ~P x <-> sngl A C_ ~P A ) )
6	4 5	mpbiri	|- ( ~P x = ~P A -> sngl A C_ ~P x )
7	6	eximi	|- ( E. x ~P x = ~P A -> E. x sngl A C_ ~P x )
8		vpwex	|- ~P x e. _V
9	8	ssex	|- ( sngl A C_ ~P x -> sngl A e. _V )
10	9	exlimiv	|- ( E. x sngl A C_ ~P x -> sngl A e. _V )
11	3 7 10	3syl	|- ( E. x x = A -> sngl A e. _V )
12	1 11	sylbi	|- ( A e. _V -> sngl A e. _V )
13		bj-snglinv	|- A = { y | { y } e. sngl A }
14		bj-snsetex	|- ( sngl A e. _V -> { y | { y } e. sngl A } e. _V )
15	13 14	eqeltrid	|- ( sngl A e. _V -> A e. _V )
16	12 15	impbii	|- ( A e. _V <-> sngl A e. _V )