Theorem bj-tagex

Description: A class is a set if and only if its tagging is a set. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-tagex	⊢ ( 𝐴 ∈ V ↔ tag 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		bj-snglex	⊢ ( 𝐴 ∈ V ↔ sngl 𝐴 ∈ V )
2		p0ex	⊢ { ∅ } ∈ V
3	2	biantru	⊢ ( sngl 𝐴 ∈ V ↔ ( sngl 𝐴 ∈ V ∧ { ∅ } ∈ V ) )
4	1 3	bitri	⊢ ( 𝐴 ∈ V ↔ ( sngl 𝐴 ∈ V ∧ { ∅ } ∈ V ) )
5		unexb	⊢ ( ( sngl 𝐴 ∈ V ∧ { ∅ } ∈ V ) ↔ ( sngl 𝐴 ∪ { ∅ } ) ∈ V )
6		df-bj-tag	⊢ tag 𝐴 = ( sngl 𝐴 ∪ { ∅ } )
7	6	eqcomi	⊢ ( sngl 𝐴 ∪ { ∅ } ) = tag 𝐴
8	7	eleq1i	⊢ ( ( sngl 𝐴 ∪ { ∅ } ) ∈ V ↔ tag 𝐴 ∈ V )
9	4 5 8	3bitri	⊢ ( 𝐴 ∈ V ↔ tag 𝐴 ∈ V )