Theorem rspc2ev

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

	Ref	Expression
Hypotheses	rspc2v.1	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
	rspc2v.2	$$⊢y=B\to \left(\chi \leftrightarrow \psi \right)$$
Assertion	rspc2ev	$$⊢\left(A\in C\wedge B\in D\wedge \psi \right)\to \exists x\in C\exists y\in D\phi$$

Proof

Step	Hyp	Ref	Expression
1		rspc2v.1	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
2		rspc2v.2	$$⊢y=B\to \left(\chi \leftrightarrow \psi \right)$$
3	2	rspcev	$$⊢\left(B\in D\wedge \psi \right)\to \exists y\in D\chi$$
4	3	anim2i	$$⊢\left(A\in C\wedge \left(B\in D\wedge \psi \right)\right)\to \left(A\in C\wedge \exists y\in D\chi \right)$$
5	4	3impb	$$⊢\left(A\in C\wedge B\in D\wedge \psi \right)\to \left(A\in C\wedge \exists y\in D\chi \right)$$
6	1	rexbidv	$$⊢x=A\to \left(\exists y\in D\phi \leftrightarrow \exists y\in D\chi \right)$$
7	6	rspcev	$$⊢\left(A\in C\wedge \exists y\in D\chi \right)\to \exists x\in C\exists y\in D\phi$$
8	5 7	syl	$$⊢\left(A\in C\wedge B\in D\wedge \psi \right)\to \exists x\in C\exists y\in D\phi$$