Theorem suceq 4362

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

Assertion

Ref	Expression
suceq	|- ( A = B -> suc A = suc B )

Proof of Theorem suceq

Step	Hyp	Ref	Expression
1		id 19	. . 3 |- ( A = B -> A = B )
2		sneq 3571	. . 3 |- ( A = B -> { A } = { B } )
3	1, 2	uneq12d 3262	. 2 |- ( A = B -> ( A u. { A } ) = ( B u. { B } ) )
4		df-suc 4331	. 2 |- suc A = ( A u. { A } )
5		df-suc 4331	. 2 |- suc B = ( B u. { B } )
6	3, 4, 5	3eqtr4g 2215	1 |- ( A = B -> suc A = suc B )

Syntax hints:   -> wi 4   = wceq 1335   u. cun 3100   {csn 3560   suc csuc 4325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3566  df-suc 4331

This theorem is referenced by:  eqelsuc  4379  2ordpr  4482  onsucsssucexmid  4485  onsucelsucexmid  4488  ordsucunielexmid  4489  suc11g  4515  onsucuni2  4522  0elsucexmid  4523  ordpwsucexmid  4528  peano2  4553  findes  4561  nn0suc  4562  0elnn  4577  omsinds  4580  tfr1onlemsucaccv  6285  tfrcllemsucaccv  6298  tfrcl  6308  frecabcl  6343  frecsuc  6351  sucinc  6389  sucinc2  6390  oacl  6404  oav2  6407  oasuc  6408  oa1suc  6411  nna0r  6422  nnacom  6428  nnaass  6429  nnmsucr  6432  nnsucelsuc  6435  nnsucsssuc  6436  nnaword  6455  nnaordex  6471  phplem3g  6798  nneneq  6799  php5  6800  php5dom  6805  omp1eomlem  7032  omp1eom  7033  nnnninfeq  7065  nnnninfeq2  7066  indpi  7256  ennnfoneleminc  12123  ennnfonelemex  12126  bj-indsuc  13474  bj-bdfindes  13495  bj-nn0suc0  13496  bj-peano4  13501  bj-inf2vnlem1  13516  bj-nn0sucALT  13524  bj-findes  13527  nnsf  13548  nninfsellemdc  13553  nninfself  13556  nninfsellemeqinf  13559  nninfomni  13562