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

Metamath Proof Explorer

Theorem raleqdv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005)

Ref Expression
Hypothesis raleqdv.1 ⊢ φ → A = B
Assertion raleqdv ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 raleqdv.1 ⊢ φ → A = B
2 raleq ⊢ A = B → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ
3 1 2 syl ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ