Theorem rspc2

Description: Restricted specialization with two quantifiers, using implicit substitution. (Contributed by NM, 9-Nov-2012)

	Ref	Expression
Hypotheses	rspc2.1	⊢ Ⅎ 𝑥 𝜒
	rspc2.2	⊢ Ⅎ 𝑦 𝜓
	rspc2.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
	rspc2.4	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
Assertion	rspc2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rspc2.1	⊢ Ⅎ 𝑥 𝜒
2		rspc2.2	⊢ Ⅎ 𝑦 𝜓
3		rspc2.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
4		rspc2.4	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
5		nfcv	⊢ Ⅎ 𝑥 𝐷
6	5 1	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐷 𝜒
7	3	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝐷 𝜑 ↔ ∀ 𝑦 ∈ 𝐷 𝜒 ) )
8	6 7	rspc	⊢ ( 𝐴 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑦 ∈ 𝐷 𝜒 ) )
9	2 4	rspc	⊢ ( 𝐵 ∈ 𝐷 → ( ∀ 𝑦 ∈ 𝐷 𝜒 → 𝜓 ) )
10	8 9	sylan9	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜑 → 𝜓 ) )