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

Metamath Proof Explorer

Theorem raleqbidva

Description: Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 raleqbidva.1 ⊢ φ → A = B
2 raleqbidva.2 ⊢ φ ∧ x ∈ A → ψ ↔ χ
3 2 ralbidva ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ A χ
4 1 raleqdv ⊢ φ → ∀ x ∈ A χ ↔ ∀ x ∈ B χ
5 3 4 bitrd ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B χ