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

Theorem suceq 5505
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 23 . . 3  |-  ( A  =  B  ->  A  =  B )
2 sneq 4007 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3622 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 5446 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 5446 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2489 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1438    u. cun 3435   {csn 3997   suc csuc 5442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-un 3442  df-sn 3998  df-suc 5446
This theorem is referenced by:  eqelsuc  5521  suc11  5543  ordunisuc  6671  onsucuni2  6673  onuninsuci  6679  limsuc  6688  tfindes  6701  tfinds2  6702  findes  6735  onnseq  7069  seqomlem0  7172  seqomlem1  7173  seqomlem4  7176  oasuc  7232  onasuc  7236  oa1suc  7239  oa0r  7246  oaass  7268  oneo  7288  omeulem1  7289  oeeulem  7308  oeeui  7309  nna0r  7316  nnacom  7324  nnaass  7329  nnmsucr  7332  omabs  7354  nnneo  7358  nneob  7359  omsmolem  7360  omopthlem1  7362  limensuc  7753  infensuc  7754  nneneq  7759  unblem2  7828  unblem3  7829  suc11reg  8128  inf0  8130  inf3lem1  8137  dfom3  8156  cantnflt  8180  cantnflem1  8197  cnfcom  8208  r1elwf  8270  rankidb  8274  rankonidlem  8302  ranklim  8318  rankopb  8326  rankelop  8348  rankxpu  8350  rankmapu  8352  rankxplim  8353  cardsucnn  8422  dif1card  8444  infxpenlem  8447  fseqenlem1  8457  dfac12lem1  8575  dfac12lem2  8576  dfac12r  8578  pwsdompw  8636  ackbij1lem5  8656  ackbij1lem14  8665  ackbij1lem18  8669  ackbij1  8670  ackbij2lem3  8673  cfsmolem  8702  cfsmo  8703  sornom  8709  isfin3ds  8761  isf32lem1  8785  isf32lem2  8786  isf32lem5  8789  isf32lem6  8790  isf32lem7  8791  isf32lem8  8792  isf32lem11  8795  fin1a2lem1  8832  ituniiun  8854  axdc2lem  8880  axdc3lem2  8883  axdc3lem3  8884  axdc3lem4  8885  axdc3  8886  axdc4lem  8887  axcclem  8889  axdclem2  8952  wunex2  9165  om2uzsuci  12163  axdc4uzlem  12196  bnj222  29696  bnj966  29757  bnj1112  29794  nofulllem1  30590  nofulllem2  30591  rankaltopb  30745  ranksng  30933  rankpwg  30935  rankeq1o  30937  ontgsucval  31091  onsuccon  31097  onsucsuccmp  31103  limsucncmp  31105  ordcmp  31106  limsuc2  35825  aomclem4  35841  aomclem8  35845
  Copyright terms: Public domain W3C validator