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

Theorem suceq 4929
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 4020 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3641 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4870 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4870 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2507 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    u. cun 3456   {csn 4010   suc csuc 4866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-un 3463  df-sn 4011  df-suc 4870
This theorem is referenced by:  eqelsuc  4945  suc11  4967  ordunisuc  6648  onsucuni2  6650  onuninsuci  6656  limsuc  6665  tfindes  6678  tfinds2  6679  findes  6711  onnseq  7013  seqomlem0  7112  seqomlem1  7113  seqomlem4  7116  oasuc  7172  onasuc  7176  oa1suc  7179  oa0r  7186  oaass  7208  oneo  7228  omeulem1  7229  oeeulem  7248  oeeui  7249  nna0r  7256  nnacom  7264  nnaass  7269  nnmsucr  7272  omabs  7294  nnneo  7298  nneob  7299  omsmolem  7300  omopthlem1  7302  limensuc  7692  infensuc  7693  nneneq  7698  unblem2  7771  unblem3  7772  suc11reg  8034  inf0  8036  inf3lem1  8043  dfom3  8062  cantnflt  8089  cantnflem1  8106  cantnfltOLD  8119  cantnflem1OLD  8129  cnfcom  8142  cnfcomOLD  8150  r1elwf  8212  rankidb  8216  rankonidlem  8244  ranklim  8260  rankopb  8268  rankelop  8290  rankxpu  8292  rankmapu  8294  rankxplim  8295  cardsucnn  8364  dif1card  8386  infxpenlem  8389  fseqenlem1  8403  dfac12lem1  8521  dfac12lem2  8522  dfac12r  8524  pwsdompw  8582  ackbij1lem5  8602  ackbij1lem14  8611  ackbij1lem18  8615  ackbij1  8616  ackbij2lem3  8619  cfsmolem  8648  cfsmo  8649  sornom  8655  isfin3ds  8707  isf32lem1  8731  isf32lem2  8732  isf32lem5  8735  isf32lem6  8736  isf32lem7  8737  isf32lem8  8738  isf32lem11  8741  fin1a2lem1  8778  ituniiun  8800  axdc2lem  8826  axdc3lem2  8829  axdc3lem3  8830  axdc3lem4  8831  axdc3  8832  axdc4lem  8833  axcclem  8835  axdclem2  8898  wunex2  9114  om2uzsuci  12033  axdc4uzlem  12066  nofulllem1  29430  nofulllem2  29431  rankaltopb  29597  ranksng  29792  rankpwg  29794  rankeq1o  29796  ontgsucval  29865  onsuccon  29871  onsucsuccmp  29877  limsucncmp  29879  ordcmp  29880  limsuc2  30954  aomclem4  30971  aomclem8  30975  bnj222  33648  bnj966  33709  bnj1112  33746
  Copyright terms: Public domain W3C validator