Metamath Proof Explorer


Theorem wsuceq1

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

Ref Expression
Assertion wsuceq1 R=SwsucRAX=wsucSAX

Proof

Step Hyp Ref Expression
1 eqid A=A
2 eqid X=X
3 wsuceq123 R=SA=AX=XwsucRAX=wsucSAX
4 1 2 3 mp3an23 R=SwsucRAX=wsucSAX