Metamath Proof Explorer


Theorem raleqdv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005)

Ref Expression
Hypothesis raleqdv.1 φA=B
Assertion raleqdv φxAψxBψ

Proof

Step Hyp Ref Expression
1 raleqdv.1 φA=B
2 raleq A=BxAψxBψ
3 1 2 syl φxAψxBψ