Theorem bj-taginv

Description: Inverse of tagging. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-taginv	$$⊢A=\left\{x|\left\{x\right\}\in tagA\right\}$$

Proof

Step	Hyp	Ref	Expression
1		bj-snglinv	$$⊢A=\left\{x|\left\{x\right\}\in snglA\right\}$$
2		bj-sngltag	$$⊢x\in \mathrm{V}\to \left(\left\{x\right\}\in snglA\leftrightarrow \left\{x\right\}\in tagA\right)$$
3	2	elv	$$⊢\left\{x\right\}\in snglA\leftrightarrow \left\{x\right\}\in tagA$$
4	3	abbii	$$⊢\left\{x|\left\{x\right\}\in snglA\right\}=\left\{x|\left\{x\right\}\in tagA\right\}$$
5	1 4	eqtri	$$⊢A=\left\{x|\left\{x\right\}\in tagA\right\}$$