Theorem suceq 4450

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 3644	. . 3 |- ( A = B -> { A } = { B } )
3	1, 2	uneq12d 3328	. 2 |- ( A = B -> ( A u. { A } ) = ( B u. { B } ) )
4		df-suc 4419	. 2 |- suc A = ( A u. { A } )
5		df-suc 4419	. 2 |- suc B = ( B u. { B } )
6	3, 4, 5	3eqtr4g 2263	1 |- ( A = B -> suc A = suc B )

Syntax hints:   -> wi 4   = wceq 1373   u. cun 3164   {csn 3633   suc csuc 4413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-suc 4419

This theorem is referenced by:  eqelsuc  4467  2ordpr  4573  onsucsssucexmid  4576  onsucelsucexmid  4579  ordsucunielexmid  4580  suc11g  4606  onsucuni2  4613  0elsucexmid  4614  ordpwsucexmid  4619  peano2  4644  findes  4652  nn0suc  4653  0elnn  4668  omsinds  4671  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  tfrcl  6452  frecabcl  6487  frecsuc  6495  sucinc  6533  sucinc2  6534  oacl  6548  oav2  6551  oasuc  6552  oa1suc  6555  nna0r  6566  nnacom  6572  nnaass  6573  nnmsucr  6576  nnsucelsuc  6579  nnsucsssuc  6580  nnaword  6599  nnaordex  6616  phplem3g  6955  nneneq  6956  php5  6957  php5dom  6962  omp1eomlem  7198  omp1eom  7199  nninfninc  7227  nnnninfeq  7232  nnnninfeq2  7233  nninfwlpoimlemg  7279  nninfwlpoimlemginf  7280  nninfwlpoim  7283  nninfinfwlpo  7284  indpi  7457  ennnfoneleminc  12815  ennnfonelemex  12818  bj-indsuc  15901  bj-bdfindes  15922  bj-nn0suc0  15923  bj-peano4  15928  bj-inf2vnlem1  15943  bj-nn0sucALT  15951  bj-findes  15954  nnsf  15979  nninfsellemdc  15984  nninfself  15987  nninfsellemeqinf  15990  nninfomni  15993