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

Theorem suceq 4580
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 20 . . 3  |-  ( A  =  B  ->  A  =  B )
2 sneq 3761 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3438 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4521 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4521 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2437 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    u. cun 3254   {csn 3750   suc csuc 4517
This theorem is referenced by:  eqelsuc  4596  suc11  4618  ordunisuc  4745  onsucuni2  4747  onuninsuci  4753  limsuc  4762  tfindes  4775  tfinds2  4776  findes  4808  onnseq  6535  seqomlem0  6635  seqomlem1  6636  seqomlem4  6639  oasuc  6697  onasuc  6701  oa1suc  6704  oa0r  6711  oaass  6733  oneo  6753  omeulem1  6754  oeeulem  6773  oeeui  6774  nna0r  6781  nnacom  6789  nnaass  6794  nnmsucr  6797  omabs  6819  nnneo  6823  nneob  6824  omsmolem  6825  omopthlem1  6827  limensuc  7213  infensuc  7214  nneneq  7219  unblem2  7289  unblem3  7290  suc11reg  7500  inf0  7502  inf3lem1  7509  dfom3  7528  cantnflt  7553  cantnflem1  7571  cnfcom  7583  r1elwf  7648  rankidb  7652  rankonidlem  7680  ranklim  7696  rankopb  7704  rankelop  7726  rankxpu  7728  rankxplim  7729  cardsucnn  7798  dif1card  7818  infxpenlem  7821  fseqenlem1  7831  dfac12lem1  7949  dfac12lem2  7950  dfac12r  7952  pwsdompw  8010  ackbij1lem5  8030  ackbij1lem14  8039  ackbij1lem18  8043  ackbij1  8044  ackbij2lem3  8047  cfsmolem  8076  cfsmo  8077  sornom  8083  isfin3ds  8135  isf32lem1  8159  isf32lem2  8160  isf32lem5  8163  isf32lem6  8164  isf32lem7  8165  isf32lem8  8166  isf32lem11  8169  fin1a2lem1  8206  ituniiun  8228  axdc2lem  8254  axdc3lem2  8257  axdc3lem3  8258  axdc3lem4  8259  axdc3  8260  axdc4lem  8261  axcclem  8263  axdclem2  8326  wunex2  8539  om2uzsuci  11208  axdc4uzlem  11241  nofulllem1  25373  nofulllem2  25374  rankaltopb  25531  ranksng  25815  rankpwg  25817  rankeq1o  25819  ontgsucval  25889  onsuccon  25895  onsucsuccmp  25901  limsucncmp  25903  ordcmp  25904  limsuc2  26799  aomclem4  26816  aomclem8  26821  bnj222  28585  bnj966  28646  bnj1112  28683
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-un 3261  df-sn 3756  df-suc 4521
  Copyright terms: Public domain W3C validator