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

Metamath Proof Explorer

Theorem rspc2v

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

Ref Expression
Hypotheses rspc2v.1 ⊢ x = A → φ ↔ χ
rspc2v.2 ⊢ y = B → χ ↔ ψ
Assertion rspc2v ⊢ A ∈ C ∧ B ∈ D → ∀ x ∈ C ∀ y ∈ D φ → ψ

Proof

Step Hyp Ref Expression
1 rspc2v.1 ⊢ x = A → φ ↔ χ
2 rspc2v.2 ⊢ y = B → χ ↔ ψ
3 1 ralbidv ⊢ x = A → ∀ y ∈ D φ ↔ ∀ y ∈ D χ
4 3 rspcv ⊢ A ∈ C → ∀ x ∈ C ∀ y ∈ D φ → ∀ y ∈ D χ
5 2 rspcv ⊢ B ∈ D → ∀ y ∈ D χ → ψ
6 4 5 sylan9 ⊢ A ∈ C ∧ B ∈ D → ∀ x ∈ C ∀ y ∈ D φ → ψ