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

Metamath Proof Explorer

Theorem raleqbid

Description: Equality deduction for restricted universal quantifier. See raleqbidv for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017)

Ref Expression
Hypotheses raleqbid.0 ⊢ Ⅎ x φ
raleqbid.1 ⊢ Ⅎ _ x A
raleqbid.2 ⊢ Ⅎ _ x B
raleqbid.3 ⊢ φ → A = B
raleqbid.4 ⊢ φ → ψ ↔ χ
Assertion raleqbid ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B χ

Proof

Step Hyp Ref Expression
1 raleqbid.0 ⊢ Ⅎ x φ
2 raleqbid.1 ⊢ Ⅎ _ x A
3 raleqbid.2 ⊢ Ⅎ _ x B
4 raleqbid.3 ⊢ φ → A = B
5 raleqbid.4 ⊢ φ → ψ ↔ χ
6 2 3 raleqf ⊢ A = B → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ
7 4 6 syl ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ
8 1 5 ralbid ⊢ φ → ∀ x ∈ B ψ ↔ ∀ x ∈ B χ
9 7 8 bitrd ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B χ