elab6g

Description: Membership in a class abstraction. Class version of sb6 . (Contributed by SN, 5-Oct-2024)

		Ref	Expression
	Assertion	elab6g	$⊢ A \in V \to (A \in \{x \| φ\} \leftrightarrow \forall x (x = A \to φ))$

Step	Hyp	Ref	Expression
1		eleq1	$⊢ y = A \to (y \in \{x \| φ\} \leftrightarrow A \in \{x \| φ\})$
2		eqeq2	$⊢ y = A \to (x = y \leftrightarrow x = A)$
3	2	imbi1d	$⊢ y = A \to ((x = y \to φ) \leftrightarrow (x = A \to φ))$
4	3	albidv	$⊢ y = A \to (\forall x (x = y \to φ) \leftrightarrow \forall x (x = A \to φ))$
5		df-clab	$⊢ y \in \{x \| φ\} \leftrightarrow [y/ x] φ$
6		sb6	$⊢ [y/ x] φ \leftrightarrow \forall x (x = y \to φ)$
7	5 6	bitri	$⊢ y \in \{x \| φ\} \leftrightarrow \forall x (x = y \to φ)$
8	1 4 7	vtoclbg	$⊢ A \in V \to (A \in \{x \| φ\} \leftrightarrow \forall x (x = A \to φ))$

Metamath Proof Explorer