Metamath Proof Explorer

Theorem cbvrexdva2OLD

Description: Obsolete version of cbvrexdva2 as of 8-Jan-2025. (Contributed by David Moews, 1-May-2017) (Proof shortened by Wolf Lammen, 12-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	cbvraldva2.1	$⊢ (φ \land x = y) \to (ψ \leftrightarrow χ)$
		cbvraldva2.2	$⊢ (φ \land x = y) \to A = B$
	Assertion	cbvrexdva2OLD	$⊢ φ \to (\exists x \in A ψ \leftrightarrow \exists y \in B χ)$

Proof

Step	Hyp	Ref	Expression
1		cbvraldva2.1	$⊢ (φ \land x = y) \to (ψ \leftrightarrow χ)$
2		cbvraldva2.2	$⊢ (φ \land x = y) \to A = B$
3		simpr	$⊢ (φ \land x = y) \to x = y$
4	3 2	eleq12d	$⊢ (φ \land x = y) \to (x \in A \leftrightarrow y \in B)$
5	4 1	anbi12d	$⊢ (φ \land x = y) \to ((x \in A \land ψ) \leftrightarrow (y \in B \land χ))$
6	5	ancoms	$⊢ (x = y \land φ) \to ((x \in A \land ψ) \leftrightarrow (y \in B \land χ))$
7	6	pm5.32da	$⊢ x = y \to ((φ \land (x \in A \land ψ)) \leftrightarrow (φ \land (y \in B \land χ)))$
8	7	cbvexvw	$⊢ \exists x (φ \land (x \in A \land ψ)) \leftrightarrow \exists y (φ \land (y \in B \land χ))$
9		19.42v	$⊢ \exists x (φ \land (x \in A \land ψ)) \leftrightarrow (φ \land \exists x (x \in A \land ψ))$
10		19.42v	$⊢ \exists y (φ \land (y \in B \land χ)) \leftrightarrow (φ \land \exists y (y \in B \land χ))$
11	8 9 10	3bitr3i	$⊢ (φ \land \exists x (x \in A \land ψ)) \leftrightarrow (φ \land \exists y (y \in B \land χ))$
12		pm5.32	$⊢ (φ \to (\exists x (x \in A \land ψ) \leftrightarrow \exists y (y \in B \land χ))) \leftrightarrow ((φ \land \exists x (x \in A \land ψ)) \leftrightarrow (φ \land \exists y (y \in B \land χ)))$
13	11 12	mpbir	$⊢ φ \to (\exists x (x \in A \land ψ) \leftrightarrow \exists y (y \in B \land χ))$
14		df-rex	$⊢ \exists x \in A ψ \leftrightarrow \exists x (x \in A \land ψ)$
15		df-rex	$⊢ \exists y \in B χ \leftrightarrow \exists y (y \in B \land χ)$
16	13 14 15	3bitr4g	$⊢ φ \to (\exists x \in A ψ \leftrightarrow \exists y \in B χ)$