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

Metamath Proof Explorer

Theorem raleqd

Description: Equality deduction for restricted universal quantifier. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses raleqd.a ⊢ Ⅎ _ x A
raleqd.b ⊢ Ⅎ _ x B
raleqd.e ⊢ φ → A = B
Assertion raleqd ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 raleqd.a ⊢ Ⅎ _ x A
2 raleqd.b ⊢ Ⅎ _ x B
3 raleqd.e ⊢ φ → A = B
4 1 2 raleqf ⊢ A = B → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ
5 3 4 syl ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ