Theorem bj-abex

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

	Ref	Expression
Assertion	bj-abex	$$⊢\left\{x|\phi \right\}\in \mathrm{V}\leftrightarrow \exists y\forall x\left(x\in y\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		isset	$$⊢\left\{x|\phi \right\}\in \mathrm{V}\leftrightarrow \exists yy=\left\{x|\phi \right\}$$
2		eqabb	$$⊢y=\left\{x|\phi \right\}\leftrightarrow \forall x\left(x\in y\leftrightarrow \phi \right)$$
3	2	exbii	$$⊢\exists yy=\left\{x|\phi \right\}\leftrightarrow \exists y\forall x\left(x\in y\leftrightarrow \phi \right)$$
4	1 3	bitri	$$⊢\left\{x|\phi \right\}\in \mathrm{V}\leftrightarrow \exists y\forall x\left(x\in y\leftrightarrow \phi \right)$$