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

Metamath Proof Explorer

Theorem riotaeqbidv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011)

Ref Expression
Hypotheses riotaeqbidv.1 ⊢ φ → A = B
riotaeqbidv.2 ⊢ φ → ψ ↔ χ
Assertion riotaeqbidv ⊢ φ → ι x ∈ A | ψ = ι x ∈ B | χ

Proof

Step Hyp Ref Expression
1 riotaeqbidv.1 ⊢ φ → A = B
2 riotaeqbidv.2 ⊢ φ → ψ ↔ χ
3 2 riotabidv ⊢ φ → ι x ∈ A | ψ = ι x ∈ A | χ
4 1 riotaeqdv ⊢ φ → ι x ∈ A | χ = ι x ∈ B | χ
5 3 4 eqtrd ⊢ φ → ι x ∈ A | ψ = ι x ∈ B | χ