MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  suceq Unicode version

Theorem suceq 4457
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
StepHypRef Expression
1 id 19 . . 3  |-  ( A  =  B  ->  A  =  B )
2 sneq 3651 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3330 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4398 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4398 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2340 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    u. cun 3150   {csn 3640   suc csuc 4394
This theorem is referenced by:  eqelsuc  4473  suc11  4496  ordunisuc  4623  onsucuni2  4625  onuninsuci  4631  limsuc  4640  tfindes  4653  tfinds2  4654  findes  4686  onnseq  6361  seqomlem0  6461  seqomlem1  6462  seqomlem4  6465  oasuc  6523  onasuc  6527  oa1suc  6530  oa0r  6537  oaass  6559  oneo  6579  omeulem1  6580  oeeulem  6599  oeeui  6600  nna0r  6607  nnacom  6615  nnaass  6620  nnmsucr  6623  omabs  6645  nnneo  6649  nneob  6650  omsmolem  6651  omopthlem1  6653  limensuc  7038  infensuc  7039  nneneq  7044  unblem2  7110  unblem3  7111  suc11reg  7320  inf0  7322  inf3lem1  7329  dfom3  7348  cantnflt  7373  cantnflem1  7391  cnfcom  7403  r1elwf  7468  rankidb  7472  rankonidlem  7500  ranklim  7516  rankopb  7524  rankelop  7546  rankxpu  7548  rankxplim  7549  cardsucnn  7618  dif1card  7638  infxpenlem  7641  fseqenlem1  7651  dfac12lem1  7769  dfac12lem2  7770  dfac12r  7772  pwsdompw  7830  ackbij1lem5  7850  ackbij1lem14  7859  ackbij1lem18  7863  ackbij1  7864  ackbij2lem3  7867  cfsmolem  7896  cfsmo  7897  sornom  7903  isfin3ds  7955  isf32lem1  7979  isf32lem2  7980  isf32lem5  7983  isf32lem6  7984  isf32lem7  7985  isf32lem8  7986  isf32lem11  7989  fin1a2lem1  8026  ituniiun  8048  axdc2lem  8074  axdc3lem2  8077  axdc3lem3  8078  axdc3lem4  8079  axdc3  8080  axdc4lem  8081  axcclem  8083  axdclem2  8147  wunex2  8360  om2uzsuci  11011  axdc4uzlem  11044  nofulllem1  24356  nofulllem2  24357  rankaltopb  24513  ranksng  24797  rankpwg  24799  rankeq1o  24801  ontgsucval  24871  onsuccon  24877  onsucsuccmp  24883  limsucncmp  24885  ordcmp  24886  tartarmap  25888  limsuc2  27137  aomclem4  27154  aomclem8  27159  bnj222  28915  bnj966  28976  bnj1112  29013
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-suc 4398
  Copyright terms: Public domain W3C validator