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 \in V \leftrightarrow tag A \in V$

Step	Hyp	Ref	Expression
1		bj-snglex	$⊢ A \in V \leftrightarrow sngl A \in V$
2		p0ex	$⊢ \{\emptyset\} \in V$
3	2	biantru	$⊢ sngl A \in V \leftrightarrow (sngl A \in V \land \{\emptyset\} \in V)$
4	1 3	bitri	$⊢ A \in V \leftrightarrow (sngl A \in V \land \{\emptyset\} \in V)$
5		unexb	$⊢ (sngl A \in V \land \{\emptyset\} \in V) \leftrightarrow sngl A \cup \{\emptyset\} \in V$
6		df-bj-tag	$⊢ tag A = sngl A \cup \{\emptyset\}$
7	6	eqcomi	$⊢ sngl A \cup \{\emptyset\} = tag A$
8	7	eleq1i	$⊢ sngl A \cup \{\emptyset\} \in V \leftrightarrow tag A \in V$
9	4 5 8	3bitri	$⊢ A \in V \leftrightarrow tag A \in V$

Metamath Proof Explorer