Metamath Proof Explorer

Theorem rexab2OLD

Description: Obsolete version of rexab2 as of 1-Dec-2023. (Contributed by Mario Carneiro, 3-Sep-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ralab2.1	$⊢ x = y \to (ψ \leftrightarrow χ)$
	Assertion	rexab2OLD	$⊢ \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		eleq1w	$⊢ 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 χ)$