ceqsrex2v

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005)

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

Step	Hyp	Ref	Expression
1		ceqsrex2v.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		ceqsrex2v.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		anass	$⊢ ((x = A \land y = B) \land φ) \leftrightarrow (x = A \land (y = B \land φ))$
4	3	rexbii	$⊢ \exists y \in D ((x = A \land y = B) \land φ) \leftrightarrow \exists y \in D (x = A \land (y = B \land φ))$
5		r19.42v	$⊢ \exists y \in D (x = A \land (y = B \land φ)) \leftrightarrow (x = A \land \exists y \in D (y = B \land φ))$
6	4 5	bitri	$⊢ \exists y \in D ((x = A \land y = B) \land φ) \leftrightarrow (x = A \land \exists y \in D (y = B \land φ))$
7	6	rexbii	$⊢ \exists x \in C \exists y \in D ((x = A \land y = B) \land φ) \leftrightarrow \exists x \in C (x = A \land \exists y \in D (y = B \land φ))$
8	1	anbi2d	$⊢ x = A \to ((y = B \land φ) \leftrightarrow (y = B \land ψ))$
9	8	rexbidv	$⊢ x = A \to (\exists y \in D (y = B \land φ) \leftrightarrow \exists y \in D (y = B \land ψ))$
10	9	ceqsrexv	$⊢ A \in C \to (\exists x \in C (x = A \land \exists y \in D (y = B \land φ)) \leftrightarrow \exists y \in D (y = B \land ψ))$
11	7 10	bitrid	$⊢ A \in C \to (\exists x \in C \exists y \in D ((x = A \land y = B) \land φ) \leftrightarrow \exists y \in D (y = B \land ψ))$
12	2	ceqsrexv	$⊢ B \in D \to (\exists y \in D (y = B \land ψ) \leftrightarrow χ)$
13	11 12	sylan9bb	$⊢ (A \in C \land B \in D) \to (\exists x \in C \exists y \in D ((x = A \land y = B) \land φ) \leftrightarrow χ)$

Metamath Proof Explorer