Metamath Proof Explorer

Theorem predeq2

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

Ref Expression
Assertion predeq2 
|- ( A = B -> Pred ( R , A , X ) = Pred ( R , B , X ) )

Proof

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