Metamath Proof Explorer


Theorem predeq3

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

Ref Expression
Assertion predeq3
|- ( X = Y -> Pred ( R , A , X ) = Pred ( R , A , Y ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  R = R
2 eqid
 |-  A = A
3 predeq123
 |-  ( ( R = R /\ A = A /\ X = Y ) -> Pred ( R , A , X ) = Pred ( R , A , Y ) )
4 1 2 3 mp3an12
 |-  ( X = Y -> Pred ( R , A , X ) = Pred ( R , A , Y ) )