Theorem rsp2

Description: Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997)

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

Proof

Step	Hyp	Ref	Expression
1		rsp	$$⊢\forall x\in A\forall y\in B\phi \to \left(x\in A\to \forall y\in B\phi \right)$$
2		rsp	$$⊢\forall y\in B\phi \to \left(y\in B\to \phi \right)$$
3	1 2	syl6	$$⊢\forall x\in A\forall y\in B\phi \to \left(x\in A\to \left(y\in B\to \phi \right)\right)$$
4	3	impd	$$⊢\forall x\in A\forall y\in B\phi \to \left(\left(x\in A\wedge y\in B\right)\to \phi \right)$$