Theorem rspec2

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

	Ref	Expression
Hypothesis	rspec2.1	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑
Assertion	rspec2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rspec2.1	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑
2	1	rspec	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝜑 )
3	2	r19.21bi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 )