Theorem bj-clex

Description: Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-clex.1	$$⊢x\in A\leftrightarrow \phi$$
Assertion	bj-clex	$$⊢A\in \mathrm{V}\leftrightarrow \exists y\forall x\left(x\in y\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-clex.1	$$⊢x\in A\leftrightarrow \phi$$
2		isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists yy=A$$
3		dfcleq	$$⊢y=A\leftrightarrow \forall x\left(x\in y\leftrightarrow x\in A\right)$$
4	1	bibi2i	$$⊢\left(x\in y\leftrightarrow x\in A\right)\leftrightarrow \left(x\in y\leftrightarrow \phi \right)$$
5	4	albii	$$⊢\forall x\left(x\in y\leftrightarrow x\in A\right)\leftrightarrow \forall x\left(x\in y\leftrightarrow \phi \right)$$
6	3 5	bitri	$$⊢y=A\leftrightarrow \forall x\left(x\in y\leftrightarrow \phi \right)$$
7	6	exbii	$$⊢\exists yy=A\leftrightarrow \exists y\forall x\left(x\in y\leftrightarrow \phi \right)$$
8	2 7	bitri	$$⊢A\in \mathrm{V}\leftrightarrow \exists y\forall x\left(x\in y\leftrightarrow \phi \right)$$