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 u. { A } ) = ( B u. { B } ) )
4 df-suc 
 |-  suc A = ( A u. { A } )
5 df-suc 
 |-  suc B = ( B u. { B } )
6 3 4 5 3eqtr4g 
 |-  ( A = B -> suc A = suc B )