Theorem suceq 4380

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 3587	. . 3 |- ( A = B -> { A } = { B } )
3	1, 2	uneq12d 3277	. 2 |- ( A = B -> ( A u. { A } ) = ( B u. { B } ) )
4		df-suc 4349	. 2 |- suc A = ( A u. { A } )
5		df-suc 4349	. 2 |- suc B = ( B u. { B } )
6	3, 4, 5	3eqtr4g 2224	1 |- ( A = B -> suc A = suc B )

Syntax hints:   -> wi 4   = wceq 1343   u. cun 3114   {csn 3576   suc csuc 4343

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-sn 3582  df-suc 4349

This theorem is referenced by:  eqelsuc  4397  2ordpr  4501  onsucsssucexmid  4504  onsucelsucexmid  4507  ordsucunielexmid  4508  suc11g  4534  onsucuni2  4541  0elsucexmid  4542  ordpwsucexmid  4547  peano2  4572  findes  4580  nn0suc  4581  0elnn  4596  omsinds  4599  tfr1onlemsucaccv  6309  tfrcllemsucaccv  6322  tfrcl  6332  frecabcl  6367  frecsuc  6375  sucinc  6413  sucinc2  6414  oacl  6428  oav2  6431  oasuc  6432  oa1suc  6435  nna0r  6446  nnacom  6452  nnaass  6453  nnmsucr  6456  nnsucelsuc  6459  nnsucsssuc  6460  nnaword  6479  nnaordex  6495  phplem3g  6822  nneneq  6823  php5  6824  php5dom  6829  omp1eomlem  7059  omp1eom  7060  nnnninfeq  7092  nnnninfeq2  7093  indpi  7283  ennnfoneleminc  12344  ennnfonelemex  12347  bj-indsuc  13810  bj-bdfindes  13831  bj-nn0suc0  13832  bj-peano4  13837  bj-inf2vnlem1  13852  bj-nn0sucALT  13860  bj-findes  13863  nnsf  13885  nninfsellemdc  13890  nninfself  13893  nninfsellemeqinf  13896  nninfomni  13899