Theorem bj-taginv

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

	Ref	Expression
Assertion	bj-taginv	⊢ 𝐴 = { 𝑥 ∣ { 𝑥 } ∈ tag 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		bj-snglinv	⊢ 𝐴 = { 𝑥 ∣ { 𝑥 } ∈ sngl 𝐴 }
2		bj-sngltag	⊢ ( 𝑥 ∈ V → ( { 𝑥 } ∈ sngl 𝐴 ↔ { 𝑥 } ∈ tag 𝐴 ) )
3	2	elv	⊢ ( { 𝑥 } ∈ sngl 𝐴 ↔ { 𝑥 } ∈ tag 𝐴 )
4	3	abbii	⊢ { 𝑥 ∣ { 𝑥 } ∈ sngl 𝐴 } = { 𝑥 ∣ { 𝑥 } ∈ tag 𝐴 }
5	1 4	eqtri	⊢ 𝐴 = { 𝑥 ∣ { 𝑥 } ∈ tag 𝐴 }