Theorem rspc2va

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014)

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

Proof

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