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

Theorem suceq 4952
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 4042 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3655 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4893 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4893 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2523 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1395    u. cun 3469   {csn 4032   suc csuc 4889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476  df-sn 4033  df-suc 4893
This theorem is referenced by:  eqelsuc  4968  suc11  4990  ordunisuc  6666  onsucuni2  6668  onuninsuci  6674  limsuc  6683  tfindes  6696  tfinds2  6697  findes  6729  onnseq  7033  seqomlem0  7132  seqomlem1  7133  seqomlem4  7136  oasuc  7192  onasuc  7196  oa1suc  7199  oa0r  7206  oaass  7228  oneo  7248  omeulem1  7249  oeeulem  7268  oeeui  7269  nna0r  7276  nnacom  7284  nnaass  7289  nnmsucr  7292  omabs  7314  nnneo  7318  nneob  7319  omsmolem  7320  omopthlem1  7322  limensuc  7713  infensuc  7714  nneneq  7719  unblem2  7791  unblem3  7792  suc11reg  8053  inf0  8055  inf3lem1  8062  dfom3  8081  cantnflt  8108  cantnflem1  8125  cantnfltOLD  8138  cantnflem1OLD  8148  cnfcom  8161  cnfcomOLD  8169  r1elwf  8231  rankidb  8235  rankonidlem  8263  ranklim  8279  rankopb  8287  rankelop  8309  rankxpu  8311  rankmapu  8313  rankxplim  8314  cardsucnn  8383  dif1card  8405  infxpenlem  8408  fseqenlem1  8422  dfac12lem1  8540  dfac12lem2  8541  dfac12r  8543  pwsdompw  8601  ackbij1lem5  8621  ackbij1lem14  8630  ackbij1lem18  8634  ackbij1  8635  ackbij2lem3  8638  cfsmolem  8667  cfsmo  8668  sornom  8674  isfin3ds  8726  isf32lem1  8750  isf32lem2  8751  isf32lem5  8754  isf32lem6  8755  isf32lem7  8756  isf32lem8  8757  isf32lem11  8760  fin1a2lem1  8797  ituniiun  8819  axdc2lem  8845  axdc3lem2  8848  axdc3lem3  8849  axdc3lem4  8850  axdc3  8851  axdc4lem  8852  axcclem  8854  axdclem2  8917  wunex2  9133  om2uzsuci  12062  axdc4uzlem  12095  nofulllem1  29679  nofulllem2  29680  rankaltopb  29834  ranksng  30029  rankpwg  30031  rankeq1o  30033  ontgsucval  30102  onsuccon  30108  onsucsuccmp  30114  limsucncmp  30116  ordcmp  30117  limsuc2  31190  aomclem4  31207  aomclem8  31211  bnj222  34084  bnj966  34145  bnj1112  34182
  Copyright terms: Public domain W3C validator