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 φ x A | ψ = x A | χ

Proof

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