Metamath Proof Explorer


Theorem bnj602

Description: Equality theorem for the _pred function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj602 X=YpredXAR=predYAR

Proof

Step Hyp Ref Expression
1 breq2 X=YyRXyRY
2 1 rabbidv X=YyA|yRX=yA|yRY
3 df-bnj14 predXAR=yA|yRX
4 df-bnj14 predYAR=yA|yRY
5 2 3 4 3eqtr4g X=YpredXAR=predYAR