Metamath Proof Explorer

Theorem wsuceq3

Description: Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018)

Ref Expression
Assertion wsuceq3 
|- ( X = Y -> wsuc ( R , A , X ) = wsuc ( R , A , Y ) )

Proof

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