This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elabf

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994) (Revised by Mario Carneiro, 12-Oct-2016)

	Ref	Expression
Hypotheses	elabf.1	$⊢ Ⅎ x ψ$
	elabf.2	$⊢ A \in V$
	elabf.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
Assertion	elabf	$⊢ A \in \{x \| φ\} \leftrightarrow ψ$

Proof

Step	Hyp	Ref	Expression
1		elabf.1	$⊢ Ⅎ x ψ$
2		elabf.2	$⊢ A \in V$
3		elabf.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
4		nfcv	$⊢ \underline{Ⅎ} x A$
5	4 1 3	elabgf	$⊢ A \in V \to (A \in \{x \| φ\} \leftrightarrow ψ)$
6	2 5	ax-mp	$⊢ A \in \{x \| φ\} \leftrightarrow ψ$