Metamath Proof Explorer

Theorem rexrab

Description: Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Hypothesis	ralab.1	$⊢ y = x \to (φ \leftrightarrow ψ)$
	Assertion	rexrab	$⊢ \exists x \in \{y \in A \| φ\} χ \leftrightarrow \exists x \in A (ψ \land χ)$

Proof

Step	Hyp	Ref	Expression
1		ralab.1	$⊢ y = x \to (φ \leftrightarrow ψ)$
2	1	elrab	$⊢ x \in \{y \in A \| φ\} \leftrightarrow (x \in A \land ψ)$
3	2	anbi1i	$⊢ (x \in \{y \in A \| φ\} \land χ) \leftrightarrow ((x \in A \land ψ) \land χ)$
4		anass	$⊢ ((x \in A \land ψ) \land χ) \leftrightarrow (x \in A \land (ψ \land χ))$
5	3 4	bitri	$⊢ (x \in \{y \in A \| φ\} \land χ) \leftrightarrow (x \in A \land (ψ \land χ))$
6	5	rexbii2	$⊢ \exists x \in \{y \in A \| φ\} χ \leftrightarrow \exists x \in A (ψ \land χ)$