Metamath Proof Explorer


Theorem suceq

Description: Equality of successors. (Contributed by NM, 30-Aug-1993) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion suceq A = B suc A = suc B

Proof

Step Hyp Ref Expression
1 id A = B A = B
2 sneq A = B A = B
3 1 2 uneq12d A = B A A = B B
4 df-suc suc A = A A
5 df-suc suc B = B B
6 3 4 5 3eqtr4g A = B suc A = suc B