clabel

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

		Ref	Expression
	Assertion	clabel	$⊢ \{x \| φ\} \in A \leftrightarrow \exists y (y \in A \land \forall x (x \in y \leftrightarrow φ))$

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

Metamath Proof Explorer