Metamath Proof Explorer


Theorem rabbiia

Description: Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999)

Ref Expression
Hypothesis rabbiia.1 xAφψ
Assertion rabbiia xA|φ=xA|ψ

Proof

Step Hyp Ref Expression
1 rabbiia.1 xAφψ
2 1 pm5.32i xAφxAψ
3 2 abbii x|xAφ=x|xAψ
4 df-rab xA|φ=x|xAφ
5 df-rab xA|ψ=x|xAψ
6 3 4 5 3eqtr4i xA|φ=xA|ψ