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

Theorem suceq 4459
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 3653 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3332 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4400 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4400 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2342 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    u. cun 3152   {csn 3642   suc csuc 4396
This theorem is referenced by:  eqelsuc  4475  suc11  4498  ordunisuc  4625  onsucuni2  4627  onuninsuci  4633  limsuc  4642  tfindes  4655  tfinds2  4656  findes  4688  onnseq  6363  seqomlem0  6463  seqomlem1  6464  seqomlem4  6467  oasuc  6525  onasuc  6529  oa1suc  6532  oa0r  6539  oaass  6561  oneo  6581  omeulem1  6582  oeeulem  6601  oeeui  6602  nna0r  6609  nnacom  6617  nnaass  6622  nnmsucr  6625  omabs  6647  nnneo  6651  nneob  6652  omsmolem  6653  omopthlem1  6655  limensuc  7040  infensuc  7041  nneneq  7046  unblem2  7112  unblem3  7113  suc11reg  7322  inf0  7324  inf3lem1  7331  dfom3  7350  cantnflt  7375  cantnflem1  7393  cnfcom  7405  r1elwf  7470  rankidb  7474  rankonidlem  7502  ranklim  7518  rankopb  7526  rankelop  7548  rankxpu  7550  rankxplim  7551  cardsucnn  7620  dif1card  7640  infxpenlem  7643  fseqenlem1  7653  dfac12lem1  7771  dfac12lem2  7772  dfac12r  7774  pwsdompw  7832  ackbij1lem5  7852  ackbij1lem14  7861  ackbij1lem18  7865  ackbij1  7866  ackbij2lem3  7869  cfsmolem  7898  cfsmo  7899  sornom  7905  isfin3ds  7957  isf32lem1  7981  isf32lem2  7982  isf32lem5  7985  isf32lem6  7986  isf32lem7  7987  isf32lem8  7988  isf32lem11  7991  fin1a2lem1  8028  ituniiun  8050  axdc2lem  8076  axdc3lem2  8079  axdc3lem3  8080  axdc3lem4  8081  axdc3  8082  axdc4lem  8083  axcclem  8085  axdclem2  8149  wunex2  8362  om2uzsuci  11013  axdc4uzlem  11046  nofulllem1  24358  nofulllem2  24359  rankaltopb  24515  ranksng  24799  rankpwg  24801  rankeq1o  24803  ontgsucval  24873  onsuccon  24879  onsucsuccmp  24885  limsucncmp  24887  ordcmp  24888  tartarmap  25899  limsuc2  27148  aomclem4  27165  aomclem8  27170  bnj222  28988  bnj966  29049  bnj1112  29086
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-un 3159  df-sn 3648  df-suc 4400
  Copyright terms: Public domain W3C validator