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 φιxA|ψ=ιxB|χ

Proof

Step Hyp Ref Expression
1 riotaeqbidv.1 φA=B
2 riotaeqbidv.2 φψχ
3 2 riotabidv φιxA|ψ=ιxA|χ
4 1 riotaeqdv φιxA|χ=ιxB|χ
5 3 4 eqtrd φιxA|ψ=ιxB|χ