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

Metamath Proof Explorer

Theorem elab4g

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012)

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

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