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

Theorem suceq 4647
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 21 . . 3  |-  ( A  =  B  ->  A  =  B )
2 sneq 3826 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3503 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4588 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4588 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2494 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    u. cun 3319   {csn 3815   suc csuc 4584
This theorem is referenced by:  eqelsuc  4663  suc11  4686  ordunisuc  4813  onsucuni2  4815  onuninsuci  4821  limsuc  4830  tfindes  4843  tfinds2  4844  findes  4876  onnseq  6607  seqomlem0  6707  seqomlem1  6708  seqomlem4  6711  oasuc  6769  onasuc  6773  oa1suc  6776  oa0r  6783  oaass  6805  oneo  6825  omeulem1  6826  oeeulem  6845  oeeui  6846  nna0r  6853  nnacom  6861  nnaass  6866  nnmsucr  6869  omabs  6891  nnneo  6895  nneob  6896  omsmolem  6897  omopthlem1  6899  limensuc  7285  infensuc  7286  nneneq  7291  unblem2  7361  unblem3  7362  suc11reg  7575  inf0  7577  inf3lem1  7584  dfom3  7603  cantnflt  7628  cantnflem1  7646  cnfcom  7658  r1elwf  7723  rankidb  7727  rankonidlem  7755  ranklim  7771  rankopb  7779  rankelop  7801  rankxpu  7803  rankxplim  7804  cardsucnn  7873  dif1card  7893  infxpenlem  7896  fseqenlem1  7906  dfac12lem1  8024  dfac12lem2  8025  dfac12r  8027  pwsdompw  8085  ackbij1lem5  8105  ackbij1lem14  8114  ackbij1lem18  8118  ackbij1  8119  ackbij2lem3  8122  cfsmolem  8151  cfsmo  8152  sornom  8158  isfin3ds  8210  isf32lem1  8234  isf32lem2  8235  isf32lem5  8238  isf32lem6  8239  isf32lem7  8240  isf32lem8  8241  isf32lem11  8244  fin1a2lem1  8281  ituniiun  8303  axdc2lem  8329  axdc3lem2  8332  axdc3lem3  8333  axdc3lem4  8334  axdc3  8335  axdc4lem  8336  axcclem  8338  axdclem2  8401  wunex2  8614  om2uzsuci  11289  axdc4uzlem  11322  nofulllem1  25658  nofulllem2  25659  rankaltopb  25825  ranksng  26109  rankpwg  26111  rankeq1o  26113  ontgsucval  26183  onsuccon  26189  onsucsuccmp  26195  limsucncmp  26197  ordcmp  26198  limsuc2  27116  aomclem4  27133  aomclem8  27137  bnj222  29255  bnj966  29316  bnj1112  29353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-un 3326  df-sn 3821  df-suc 4588
  Copyright terms: Public domain W3C validator