Theorem bj-sngltag

Description: The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-sngltag	$$⊢A\in V\to \left(\left\{A\right\}\in snglB\leftrightarrow \left\{A\right\}\in tagB\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-sngltagi	$$⊢\left\{A\right\}\in snglB\to \left\{A\right\}\in tagB$$
2		df-bj-tag	$$⊢tagB=snglB\cup \left\{\varnothing \right\}$$
3	2	eleq2i	$$⊢\left\{A\right\}\in tagB\leftrightarrow \left\{A\right\}\in \left(snglB\cup \left\{\varnothing \right\}\right)$$
4		elun	$$⊢\left\{A\right\}\in \left(snglB\cup \left\{\varnothing \right\}\right)\leftrightarrow \left(\left\{A\right\}\in snglB\vee \left\{A\right\}\in \left\{\varnothing \right\}\right)$$
5		idd	$$⊢A\in V\to \left(\left\{A\right\}\in snglB\to \left\{A\right\}\in snglB\right)$$
6		elsni	$$⊢\left\{A\right\}\in \left\{\varnothing \right\}\to \left\{A\right\}=\varnothing$$
7		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
8		elex	$$⊢A\in V\to A\in \mathrm{V}$$
9	8	pm2.24d	$$⊢A\in V\to \left(\neg A\in \mathrm{V}\to \left\{A\right\}\in snglB\right)$$
10	7 9	biimtrrid	$$⊢A\in V\to \left(\left\{A\right\}=\varnothing \to \left\{A\right\}\in snglB\right)$$
11	6 10	syl5	$$⊢A\in V\to \left(\left\{A\right\}\in \left\{\varnothing \right\}\to \left\{A\right\}\in snglB\right)$$
12	5 11	jaod	$$⊢A\in V\to \left(\left(\left\{A\right\}\in snglB\vee \left\{A\right\}\in \left\{\varnothing \right\}\right)\to \left\{A\right\}\in snglB\right)$$
13	4 12	biimtrid	$$⊢A\in V\to \left(\left\{A\right\}\in \left(snglB\cup \left\{\varnothing \right\}\right)\to \left\{A\right\}\in snglB\right)$$
14	3 13	biimtrid	$$⊢A\in V\to \left(\left\{A\right\}\in tagB\to \left\{A\right\}\in snglB\right)$$
15	1 14	impbid2	$$⊢A\in V\to \left(\left\{A\right\}\in snglB\leftrightarrow \left\{A\right\}\in tagB\right)$$