Metamath Proof Explorer

Theorem rexab2

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015) Drop ax-8 . (Revised by Gino Giotto, 1-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		ralab2.1	$⊢ x = y \to (ψ \leftrightarrow χ)$
2		df-rex	$⊢ \exists x \in \{y \| φ\} ψ \leftrightarrow \exists x (x \in \{y \| φ\} \land ψ)$
3		nfsab1	$⊢ Ⅎ y x \in \{y \| φ\}$
4		nfv	$⊢ Ⅎ y ψ$
5	3 4	nfan	$⊢ Ⅎ y (x \in \{y \| φ\} \land ψ)$
6		nfv	$⊢ Ⅎ x (φ \land χ)$
7		eleq1ab	$⊢ x = y \to (x \in \{y \| φ\} \leftrightarrow y \in \{y \| φ\})$
8		abid	$⊢ y \in \{y \| φ\} \leftrightarrow φ$
9	7 8	bitrdi	$⊢ x = y \to (x \in \{y \| φ\} \leftrightarrow φ)$
10	9 1	anbi12d	$⊢ x = y \to ((x \in \{y \| φ\} \land ψ) \leftrightarrow (φ \land χ))$
11	5 6 10	cbvexv1	$⊢ \exists x (x \in \{y \| φ\} \land ψ) \leftrightarrow \exists y (φ \land χ)$
12	2 11	bitri	$⊢ \exists x \in \{y \| φ\} ψ \leftrightarrow \exists y (φ \land χ)$