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	|- ( A e. _V <-> tag A e. _V )

Proof

Step	Hyp	Ref	Expression
1		bj-snglex	|- ( A e. _V <-> sngl A e. _V )
2		p0ex	|- { (/) } e. _V
3	2	biantru	|- ( sngl A e. _V <-> ( sngl A e. _V /\ { (/) } e. _V ) )
4	1 3	bitri	|- ( A e. _V <-> ( sngl A e. _V /\ { (/) } e. _V ) )
5		unexb	|- ( ( sngl A e. _V /\ { (/) } e. _V ) <-> ( sngl A u. { (/) } ) e. _V )
6		df-bj-tag	|- tag A = ( sngl A u. { (/) } )
7	6	eqcomi	|- ( sngl A u. { (/) } ) = tag A
8	7	eleq1i	|- ( ( sngl A u. { (/) } ) e. _V <-> tag A e. _V )
9	4 5 8	3bitri	|- ( A e. _V <-> tag A e. _V )