Theorem suceq 4437

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 3633	. . 3 |- ( A = B -> { A } = { B } )
3	1, 2	uneq12d 3318	. 2 |- ( A = B -> ( A u. { A } ) = ( B u. { B } ) )
4		df-suc 4406	. 2 |- suc A = ( A u. { A } )
5		df-suc 4406	. 2 |- suc B = ( B u. { B } )
6	3, 4, 5	3eqtr4g 2254	1 |- ( A = B -> suc A = suc B )

Syntax hints:   -> wi 4   = wceq 1364   u. cun 3155   {csn 3622   suc csuc 4400

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-suc 4406

This theorem is referenced by:  eqelsuc  4454  2ordpr  4560  onsucsssucexmid  4563  onsucelsucexmid  4566  ordsucunielexmid  4567  suc11g  4593  onsucuni2  4600  0elsucexmid  4601  ordpwsucexmid  4606  peano2  4631  findes  4639  nn0suc  4640  0elnn  4655  omsinds  4658  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  tfrcl  6422  frecabcl  6457  frecsuc  6465  sucinc  6503  sucinc2  6504  oacl  6518  oav2  6521  oasuc  6522  oa1suc  6525  nna0r  6536  nnacom  6542  nnaass  6543  nnmsucr  6546  nnsucelsuc  6549  nnsucsssuc  6550  nnaword  6569  nnaordex  6586  phplem3g  6917  nneneq  6918  php5  6919  php5dom  6924  omp1eomlem  7160  omp1eom  7161  nninfninc  7189  nnnninfeq  7194  nnnninfeq2  7195  nninfwlpoimlemg  7241  nninfwlpoimlemginf  7242  nninfwlpoim  7244  indpi  7409  ennnfoneleminc  12628  ennnfonelemex  12631  bj-indsuc  15574  bj-bdfindes  15595  bj-nn0suc0  15596  bj-peano4  15601  bj-inf2vnlem1  15616  bj-nn0sucALT  15624  bj-findes  15627  nnsf  15649  nninfsellemdc  15654  nninfself  15657  nninfsellemeqinf  15660  nninfomni  15663