rspc2ev

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999)

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

Step	Hyp	Ref	Expression
1		rspc2v.1	$⊢ x = A \to (φ \leftrightarrow χ)$
2		rspc2v.2	$⊢ y = B \to (χ \leftrightarrow ψ)$
3	2	rspcev	$⊢ (B \in D \land ψ) \to \exists y \in D χ$
4	3	anim2i	$⊢ (A \in C \land (B \in D \land ψ)) \to (A \in C \land \exists y \in D χ)$
5	4	3impb	$⊢ (A \in C \land B \in D \land ψ) \to (A \in C \land \exists y \in D χ)$
6	1	rexbidv	$⊢ x = A \to (\exists y \in D φ \leftrightarrow \exists y \in D χ)$
7	6	rspcev	$⊢ (A \in C \land \exists y \in D χ) \to \exists x \in C \exists y \in D φ$
8	5 7	syl	$⊢ (A \in C \land B \in D \land ψ) \to \exists x \in C \exists y \in D φ$

Metamath Proof Explorer