Theorem bj-snglc

Description: Characterization of the elements of A in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-snglc	|- ( A e. B <-> { A } e. sngl B )

Proof

Step	Hyp	Ref	Expression
1		df-rex	|- ( E. x e. B { A } = { x } <-> E. x ( x e. B /\ { A } = { x } ) )
2		bj-elsngl	|- ( { A } e. sngl B <-> E. x e. B { A } = { x } )
3		elisset	|- ( A e. B -> E. x x = A )
4	3	pm4.71i	|- ( A e. B <-> ( A e. B /\ E. x x = A ) )
5		19.42v	|- ( E. x ( A e. B /\ x = A ) <-> ( A e. B /\ E. x x = A ) )
6		eleq1	|- ( A = x -> ( A e. B <-> x e. B ) )
7	6	eqcoms	|- ( x = A -> ( A e. B <-> x e. B ) )
8	7	pm5.32ri	|- ( ( A e. B /\ x = A ) <-> ( x e. B /\ x = A ) )
9	8	exbii	|- ( E. x ( A e. B /\ x = A ) <-> E. x ( x e. B /\ x = A ) )
10	4 5 9	3bitr2i	|- ( A e. B <-> E. x ( x e. B /\ x = A ) )
11		sneqbg	|- ( x e. _V -> ( { x } = { A } <-> x = A ) )
12	11	elv	|- ( { x } = { A } <-> x = A )
13		eqcom	|- ( { x } = { A } <-> { A } = { x } )
14	12 13	bitr3i	|- ( x = A <-> { A } = { x } )
15	14	anbi2i	|- ( ( x e. B /\ x = A ) <-> ( x e. B /\ { A } = { x } ) )
16	15	exbii	|- ( E. x ( x e. B /\ x = A ) <-> E. x ( x e. B /\ { A } = { x } ) )
17	10 16	bitri	|- ( A e. B <-> E. x ( x e. B /\ { A } = { x } ) )
18	1 2 17	3bitr4ri	|- ( A e. B <-> { A } e. sngl B )