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\in snglB\leftrightarrow \exists x\in BA=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfclel	$$⊢A\in snglB\leftrightarrow \exists y\left(y=A\wedge y\in snglB\right)$$
2		df-bj-sngl	$$⊢snglB=\left\{y|\exists x\in By=\left\{x\right\}\right\}$$
3	2	abeq2i	$$⊢y\in snglB\leftrightarrow \exists x\in By=\left\{x\right\}$$
4	3	anbi2i	$$⊢\left(y=A\wedge y\in snglB\right)\leftrightarrow \left(y=A\wedge \exists x\in By=\left\{x\right\}\right)$$
5	4	exbii	$$⊢\exists y\left(y=A\wedge y\in snglB\right)\leftrightarrow \exists y\left(y=A\wedge \exists x\in By=\left\{x\right\}\right)$$
6		r19.42v	$$⊢\exists x\in B\left(y=A\wedge y=\left\{x\right\}\right)\leftrightarrow \left(y=A\wedge \exists x\in By=\left\{x\right\}\right)$$
7	6	bicomi	$$⊢\left(y=A\wedge \exists x\in By=\left\{x\right\}\right)\leftrightarrow \exists x\in B\left(y=A\wedge y=\left\{x\right\}\right)$$
8	7	exbii	$$⊢\exists y\left(y=A\wedge \exists x\in By=\left\{x\right\}\right)\leftrightarrow \exists y\exists x\in B\left(y=A\wedge y=\left\{x\right\}\right)$$
9		rexcom4	$$⊢\exists x\in B\exists y\left(y=A\wedge y=\left\{x\right\}\right)\leftrightarrow \exists y\exists x\in B\left(y=A\wedge y=\left\{x\right\}\right)$$
10	9	bicomi	$$⊢\exists y\exists x\in B\left(y=A\wedge y=\left\{x\right\}\right)\leftrightarrow \exists x\in B\exists y\left(y=A\wedge y=\left\{x\right\}\right)$$
11		eqcom	$$⊢A=\left\{x\right\}\leftrightarrow \left\{x\right\}=A$$
12		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
13	12	eqvinc	$$⊢\left\{x\right\}=A\leftrightarrow \exists y\left(y=\left\{x\right\}\wedge y=A\right)$$
14		exancom	$$⊢\exists y\left(y=\left\{x\right\}\wedge y=A\right)\leftrightarrow \exists y\left(y=A\wedge y=\left\{x\right\}\right)$$
15	11 13 14	3bitri	$$⊢A=\left\{x\right\}\leftrightarrow \exists y\left(y=A\wedge y=\left\{x\right\}\right)$$
16	15	bicomi	$$⊢\exists y\left(y=A\wedge y=\left\{x\right\}\right)\leftrightarrow A=\left\{x\right\}$$
17	16	rexbii	$$⊢\exists x\in B\exists y\left(y=A\wedge y=\left\{x\right\}\right)\leftrightarrow \exists x\in BA=\left\{x\right\}$$
18	8 10 17	3bitri	$$⊢\exists y\left(y=A\wedge \exists x\in By=\left\{x\right\}\right)\leftrightarrow \exists x\in BA=\left\{x\right\}$$
19	1 5 18	3bitri	$$⊢A\in snglB\leftrightarrow \exists x\in BA=\left\{x\right\}$$