Theorem rspc2v

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999)

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

Proof

Step	Hyp	Ref	Expression
1		rspc2v.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
2		rspc2v.2	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜓 ) )
3	1	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝐷 𝜑 ↔ ∀ 𝑦 ∈ 𝐷 𝜒 ) )
4	3	rspcv	⊢ ( 𝐴 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑦 ∈ 𝐷 𝜒 ) )
5	2	rspcv	⊢ ( 𝐵 ∈ 𝐷 → ( ∀ 𝑦 ∈ 𝐷 𝜒 → 𝜓 ) )
6	4 5	sylan9	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜑 → 𝜓 ) )