This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐷 𝜑 ) → 𝜓 )