Theorem bj-eltag

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

	Ref	Expression
Assertion	bj-eltag	$$⊢A\in tagB\leftrightarrow \left(\exists x\in BA=\left\{x\right\}\vee A=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-bj-tag	$$⊢tagB=snglB\cup \left\{\varnothing \right\}$$
2	1	eleq2i	$$⊢A\in tagB\leftrightarrow A\in \left(snglB\cup \left\{\varnothing \right\}\right)$$
3		elun	$$⊢A\in \left(snglB\cup \left\{\varnothing \right\}\right)\leftrightarrow \left(A\in snglB\vee A\in \left\{\varnothing \right\}\right)$$
4		bj-elsngl	$$⊢A\in snglB\leftrightarrow \exists x\in BA=\left\{x\right\}$$
5		0ex	$$⊢\varnothing \in \mathrm{V}$$
6	5	elsn2	$$⊢A\in \left\{\varnothing \right\}\leftrightarrow A=\varnothing$$
7	4 6	orbi12i	$$⊢\left(A\in snglB\vee A\in \left\{\varnothing \right\}\right)\leftrightarrow \left(\exists x\in BA=\left\{x\right\}\vee A=\varnothing \right)$$
8	2 3 7	3bitri	$$⊢A\in tagB\leftrightarrow \left(\exists x\in BA=\left\{x\right\}\vee A=\varnothing \right)$$