Theorem rsp2e

Description: Restricted specialization. (Contributed by FL, 4-Jun-2012) (Proof shortened by Wolf Lammen, 7-Jan-2020)

	Ref	Expression
Assertion	rsp2e	$$⊢\left(x\in A\wedge y\in B\wedge \phi \right)\to \exists x\in A\exists y\in B\phi$$

Proof

Step	Hyp	Ref	Expression
1		rspe	$$⊢\left(y\in B\wedge \phi \right)\to \exists y\in B\phi$$
2		rspe	$$⊢\left(x\in A\wedge \exists y\in B\phi \right)\to \exists x\in A\exists y\in B\phi$$
3	1 2	sylan2	$$⊢\left(x\in A\wedge \left(y\in B\wedge \phi \right)\right)\to \exists x\in A\exists y\in B\phi$$
4	3	3impb	$$⊢\left(x\in A\wedge y\in B\wedge \phi \right)\to \exists x\in A\exists y\in B\phi$$