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

Theorem suceq 4771
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 22 . . 3  |-  ( A  =  B  ->  A  =  B )
2 sneq 3875 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3499 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4712 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4712 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2490 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    u. cun 3314   {csn 3865   suc csuc 4708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-sn 3866  df-suc 4712
This theorem is referenced by:  eqelsuc  4787  suc11  4809  ordunisuc  6432  onsucuni2  6434  onuninsuci  6440  limsuc  6449  tfindes  6462  tfinds2  6463  findes  6495  onnseq  6791  seqomlem0  6890  seqomlem1  6891  seqomlem4  6894  oasuc  6952  onasuc  6956  oa1suc  6959  oa0r  6966  oaass  6988  oneo  7008  omeulem1  7009  oeeulem  7028  oeeui  7029  nna0r  7036  nnacom  7044  nnaass  7049  nnmsucr  7052  omabs  7074  nnneo  7078  nneob  7079  omsmolem  7080  omopthlem1  7082  limensuc  7476  infensuc  7477  nneneq  7482  unblem2  7553  unblem3  7554  suc11reg  7813  inf0  7815  inf3lem1  7822  dfom3  7841  cantnflt  7868  cantnflem1  7885  cantnfltOLD  7898  cantnflem1OLD  7908  cnfcom  7921  cnfcomOLD  7929  r1elwf  7991  rankidb  7995  rankonidlem  8023  ranklim  8039  rankopb  8047  rankelop  8069  rankxpu  8071  rankmapu  8073  rankxplim  8074  cardsucnn  8143  dif1card  8165  infxpenlem  8168  fseqenlem1  8182  dfac12lem1  8300  dfac12lem2  8301  dfac12r  8303  pwsdompw  8361  ackbij1lem5  8381  ackbij1lem14  8390  ackbij1lem18  8394  ackbij1  8395  ackbij2lem3  8398  cfsmolem  8427  cfsmo  8428  sornom  8434  isfin3ds  8486  isf32lem1  8510  isf32lem2  8511  isf32lem5  8514  isf32lem6  8515  isf32lem7  8516  isf32lem8  8517  isf32lem11  8520  fin1a2lem1  8557  ituniiun  8579  axdc2lem  8605  axdc3lem2  8608  axdc3lem3  8609  axdc3lem4  8610  axdc3  8611  axdc4lem  8612  axcclem  8614  axdclem2  8677  wunex2  8892  om2uzsuci  11754  axdc4uzlem  11787  nofulllem1  27689  nofulllem2  27690  rankaltopb  27856  ranksng  28051  rankpwg  28053  rankeq1o  28055  ontgsucval  28125  onsuccon  28131  onsucsuccmp  28137  limsucncmp  28139  ordcmp  28140  limsuc2  29235  aomclem4  29252  aomclem8  29256  bnj222  31575  bnj966  31636  bnj1112  31673
  Copyright terms: Public domain W3C validator