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

Metamath Proof Explorer

Theorem elab2g

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995)

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

Step	Hyp	Ref	Expression
1		elab2g.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		elab2g.2	$⊢ B = \{x \| φ\}$
3	2	eleq2i	$⊢ A \in B \leftrightarrow A \in \{x \| φ\}$
4	1	elabg	$⊢ A \in V \to (A \in \{x \| φ\} \leftrightarrow ψ)$
5	3 4	bitrid	$⊢ A \in V \to (A \in B \leftrightarrow ψ)$