Metamath Proof Explorer

Theorem clelab

Description: Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993) (Proof shortened by Wolf Lammen, 16-Nov-2019)

		Ref	Expression
	Assertion	clelab	$⊢ A \in \{x \| φ\} \leftrightarrow \exists x (x = A \land φ)$

Proof

Step	Hyp	Ref	Expression
1		dfclel	$⊢ A \in \{x \| φ\} \leftrightarrow \exists y (y = A \land y \in \{x \| φ\})$
2		nfv	$⊢ Ⅎ y (x = A \land φ)$
3		nfv	$⊢ Ⅎ x y = A$
4		nfsab1	$⊢ Ⅎ x y \in \{x \| φ\}$
5	3 4	nfan	$⊢ Ⅎ x (y = A \land y \in \{x \| φ\})$
6		eqeq1	$⊢ x = y \to (x = A \leftrightarrow y = A)$
7		sbequ12	$⊢ x = y \to (φ \leftrightarrow [y/ x] φ)$
8		df-clab	$⊢ y \in \{x \| φ\} \leftrightarrow [y/ x] φ$
9	7 8	syl6bbr	$⊢ x = y \to (φ \leftrightarrow y \in \{x \| φ\})$
10	6 9	anbi12d	$⊢ x = y \to ((x = A \land φ) \leftrightarrow (y = A \land y \in \{x \| φ\}))$
11	2 5 10	cbvexv1	$⊢ \exists x (x = A \land φ) \leftrightarrow \exists y (y = A \land y \in \{x \| φ\})$
12	1 11	bitr4i	$⊢ A \in \{x \| φ\} \leftrightarrow \exists x (x = A \land φ)$