Theorem rspec2

Description: Specialization rule for restricted quantification, with two quantifiers. (Contributed by NM, 20-Nov-1994)

	Ref	Expression
Hypothesis	rspec2.1	$$⊢\forall x\in A\forall y\in B\phi$$
Assertion	rspec2	$$⊢\left(x\in A\wedge y\in B\right)\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		rspec2.1	$$⊢\forall x\in A\forall y\in B\phi$$
2	1	rspec	$$⊢x\in A\to \forall y\in B\phi$$
3	2	r19.21bi	$$⊢\left(x\in A\wedge y\in B\right)\to \phi$$