Metamath Proof Explorer


Theorem rabbidv

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995)

Ref Expression
Hypothesis rabbidv.1 φψχ
Assertion rabbidv φxA|ψ=xA|χ

Proof

Step Hyp Ref Expression
1 rabbidv.1 φψχ
2 1 adantr φxAψχ
3 2 rabbidva φxA|ψ=xA|χ