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 | χ