Theorem bj-taginv

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

	Ref	Expression
Assertion	bj-taginv	|- A = { x | { x } e. tag A }

Proof

Step	Hyp	Ref	Expression
1		bj-snglinv	|- A = { x | { x } e. sngl A }
2		bj-sngltag	|- ( x e. _V -> ( { x } e. sngl A <-> { x } e. tag A ) )
3	2	elv	|- ( { x } e. sngl A <-> { x } e. tag A )
4	3	abbii	|- { x | { x } e. sngl A } = { x | { x } e. tag A }
5	1 4	eqtri	|- A = { x | { x } e. tag A }