rexrab2

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Step	Hyp	Ref	Expression
1		ralab2.1	$⊢ x = y \to (ψ \leftrightarrow χ)$
2		df-rab	$⊢ \{y \in A \| φ\} = \{y \| (y \in A \land φ)\}$
3	2	rexeqi	$⊢ \exists x \in \{y \in A \| φ\} ψ \leftrightarrow \exists x \in \{y \| (y \in A \land φ)\} ψ$
4	1	rexab2	$⊢ \exists x \in \{y \| (y \in A \land φ)\} ψ \leftrightarrow \exists y ((y \in A \land φ) \land χ)$
5		anass	$⊢ ((y \in A \land φ) \land χ) \leftrightarrow (y \in A \land (φ \land χ))$
6	5	exbii	$⊢ \exists y ((y \in A \land φ) \land χ) \leftrightarrow \exists y (y \in A \land (φ \land χ))$
7		df-rex	$⊢ \exists y \in A (φ \land χ) \leftrightarrow \exists y (y \in A \land (φ \land χ))$
8	6 7	bitr4i	$⊢ \exists y ((y \in A \land φ) \land χ) \leftrightarrow \exists y \in A (φ \land χ)$
9	3 4 8	3bitri	$⊢ \exists x \in \{y \in A \| φ\} ψ \leftrightarrow \exists y \in A (φ \land χ)$

Metamath Proof Explorer