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

Theorem suceq 4473
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 3664 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3343 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4414 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4414 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2353 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    u. cun 3163   {csn 3653   suc csuc 4410
This theorem is referenced by:  eqelsuc  4489  suc11  4512  ordunisuc  4639  onsucuni2  4641  onuninsuci  4647  limsuc  4656  tfindes  4669  tfinds2  4670  findes  4702  onnseq  6377  seqomlem0  6477  seqomlem1  6478  seqomlem4  6481  oasuc  6539  onasuc  6543  oa1suc  6546  oa0r  6553  oaass  6575  oneo  6595  omeulem1  6596  oeeulem  6615  oeeui  6616  nna0r  6623  nnacom  6631  nnaass  6636  nnmsucr  6639  omabs  6661  nnneo  6665  nneob  6666  omsmolem  6667  omopthlem1  6669  limensuc  7054  infensuc  7055  nneneq  7060  unblem2  7126  unblem3  7127  suc11reg  7336  inf0  7338  inf3lem1  7345  dfom3  7364  cantnflt  7389  cantnflem1  7407  cnfcom  7419  r1elwf  7484  rankidb  7488  rankonidlem  7516  ranklim  7532  rankopb  7540  rankelop  7562  rankxpu  7564  rankxplim  7565  cardsucnn  7634  dif1card  7654  infxpenlem  7657  fseqenlem1  7667  dfac12lem1  7785  dfac12lem2  7786  dfac12r  7788  pwsdompw  7846  ackbij1lem5  7866  ackbij1lem14  7875  ackbij1lem18  7879  ackbij1  7880  ackbij2lem3  7883  cfsmolem  7912  cfsmo  7913  sornom  7919  isfin3ds  7971  isf32lem1  7995  isf32lem2  7996  isf32lem5  7999  isf32lem6  8000  isf32lem7  8001  isf32lem8  8002  isf32lem11  8005  fin1a2lem1  8042  ituniiun  8064  axdc2lem  8090  axdc3lem2  8093  axdc3lem3  8094  axdc3lem4  8095  axdc3  8096  axdc4lem  8097  axcclem  8099  axdclem2  8163  wunex2  8376  om2uzsuci  11027  axdc4uzlem  11060  nofulllem1  24427  nofulllem2  24428  rankaltopb  24585  ranksng  24869  rankpwg  24871  rankeq1o  24873  ontgsucval  24943  onsuccon  24949  onsucsuccmp  24955  limsucncmp  24957  ordcmp  24958  tartarmap  25991  limsuc2  27240  aomclem4  27257  aomclem8  27262  bnj222  29231  bnj966  29292  bnj1112  29329
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-sn 3659  df-suc 4414
  Copyright terms: Public domain W3C validator