Theorem clabel

Description: Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006)

	Ref	Expression
Assertion	clabel	$$⊢\left\{x|\phi \right\}\in A\leftrightarrow \exists y\left(y\in A\wedge \forall x\left(x\in y\leftrightarrow \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfclel	$$⊢\left\{x|\phi \right\}\in A\leftrightarrow \exists y\left(y=\left\{x|\phi \right\}\wedge y\in A\right)$$
2		eqabb	$$⊢y=\left\{x|\phi \right\}\leftrightarrow \forall x\left(x\in y\leftrightarrow \phi \right)$$
3	2	anbi2ci	$$⊢\left(y=\left\{x|\phi \right\}\wedge y\in A\right)\leftrightarrow \left(y\in A\wedge \forall x\left(x\in y\leftrightarrow \phi \right)\right)$$
4	3	exbii	$$⊢\exists y\left(y=\left\{x|\phi \right\}\wedge y\in A\right)\leftrightarrow \exists y\left(y\in A\wedge \forall x\left(x\in y\leftrightarrow \phi \right)\right)$$
5	1 4	bitri	$$⊢\left\{x|\phi \right\}\in A\leftrightarrow \exists y\left(y\in A\wedge \forall x\left(x\in y\leftrightarrow \phi \right)\right)$$