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

Theorem suceq 5506
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 3989 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3600 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 5447 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 5447 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2520 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454    u. cun 3413   {csn 3979   suc csuc 5443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420  df-sn 3980  df-suc 5447
This theorem is referenced by:  eqelsuc  5522  suc11  5544  ordunisuc  6685  onsucuni2  6687  onuninsuci  6693  limsuc  6702  tfindes  6715  tfinds2  6716  findes  6749  onnseq  7088  seqomlem0  7191  seqomlem1  7192  seqomlem4  7195  oasuc  7251  onasuc  7255  oa1suc  7258  oa0r  7265  oaass  7287  oneo  7307  omeulem1  7308  oeeulem  7327  oeeui  7328  nna0r  7335  nnacom  7343  nnaass  7348  nnmsucr  7351  omabs  7373  nnneo  7377  nneob  7378  omsmolem  7379  omopthlem1  7381  limensuc  7774  infensuc  7775  nneneq  7780  unblem2  7849  unblem3  7850  suc11reg  8149  inf0  8151  inf3lem1  8158  dfom3  8177  cantnflt  8202  cantnflem1  8219  cnfcom  8230  r1elwf  8292  rankidb  8296  rankonidlem  8324  ranklim  8340  rankopb  8348  rankelop  8370  rankxpu  8372  rankmapu  8374  rankxplim  8375  cardsucnn  8444  dif1card  8466  infxpenlem  8469  fseqenlem1  8480  dfac12lem1  8598  dfac12lem2  8599  dfac12r  8601  pwsdompw  8659  ackbij1lem5  8679  ackbij1lem14  8688  ackbij1lem18  8692  ackbij1  8693  ackbij2lem3  8696  cfsmolem  8725  cfsmo  8726  sornom  8732  isfin3ds  8784  isf32lem1  8808  isf32lem2  8809  isf32lem5  8812  isf32lem6  8813  isf32lem7  8814  isf32lem8  8815  isf32lem11  8818  fin1a2lem1  8855  ituniiun  8877  axdc2lem  8903  axdc3lem2  8906  axdc3lem3  8907  axdc3lem4  8908  axdc3  8909  axdc4lem  8910  axcclem  8912  axdclem2  8975  wunex2  9188  om2uzsuci  12193  axdc4uzlem  12226  bnj222  29742  bnj966  29803  bnj1112  29840  nofulllem1  30639  nofulllem2  30640  rankaltopb  30794  ranksng  30982  rankpwg  30984  rankeq1o  30986  ontgsucval  31140  onsuccon  31146  onsucsuccmp  31152  limsucncmp  31154  ordcmp  31155  finxpreclem4  31830  finxp00  31838  limsuc2  35943  aomclem4  35959  aomclem8  35963
  Copyright terms: Public domain W3C validator