Metamath Proof Explorer


Theorem predeq2

Description: Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011)

Ref Expression
Assertion predeq2 A=BPredRAX=PredRBX

Proof

Step Hyp Ref Expression
1 eqid R=R
2 eqid X=X
3 predeq123 R=RA=BX=XPredRAX=PredRBX
4 1 2 3 mp3an13 A=BPredRAX=PredRBX