Theorem bj-elsngl

Description: Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-elsngl	|- ( A e. sngl B <-> E. x e. B A = { x } )

Proof

Step	Hyp	Ref	Expression
1		dfclel	|- ( A e. sngl B <-> E. y ( y = A /\ y e. sngl B ) )
2		df-bj-sngl	|- sngl B = { y | E. x e. B y = { x } }
3	2	abeq2i	|- ( y e. sngl B <-> E. x e. B y = { x } )
4	3	anbi2i	|- ( ( y = A /\ y e. sngl B ) <-> ( y = A /\ E. x e. B y = { x } ) )
5	4	exbii	|- ( E. y ( y = A /\ y e. sngl B ) <-> E. y ( y = A /\ E. x e. B y = { x } ) )
6		r19.42v	|- ( E. x e. B ( y = A /\ y = { x } ) <-> ( y = A /\ E. x e. B y = { x } ) )
7	6	bicomi	|- ( ( y = A /\ E. x e. B y = { x } ) <-> E. x e. B ( y = A /\ y = { x } ) )
8	7	exbii	|- ( E. y ( y = A /\ E. x e. B y = { x } ) <-> E. y E. x e. B ( y = A /\ y = { x } ) )
9		rexcom4	|- ( E. x e. B E. y ( y = A /\ y = { x } ) <-> E. y E. x e. B ( y = A /\ y = { x } ) )
10	9	bicomi	|- ( E. y E. x e. B ( y = A /\ y = { x } ) <-> E. x e. B E. y ( y = A /\ y = { x } ) )
11		eqcom	|- ( A = { x } <-> { x } = A )
12		snex	|- { x } e. _V
13	12	eqvinc	|- ( { x } = A <-> E. y ( y = { x } /\ y = A ) )
14		exancom	|- ( E. y ( y = { x } /\ y = A ) <-> E. y ( y = A /\ y = { x } ) )
15	11 13 14	3bitri	|- ( A = { x } <-> E. y ( y = A /\ y = { x } ) )
16	15	bicomi	|- ( E. y ( y = A /\ y = { x } ) <-> A = { x } )
17	16	rexbii	|- ( E. x e. B E. y ( y = A /\ y = { x } ) <-> E. x e. B A = { x } )
18	8 10 17	3bitri	|- ( E. y ( y = A /\ E. x e. B y = { x } ) <-> E. x e. B A = { x } )
19	1 5 18	3bitri	|- ( A e. sngl B <-> E. x e. B A = { x } )