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

Theorem suceq 4638
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 20 . . 3  |-  ( A  =  B  ->  A  =  B )
2 sneq 3817 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3494 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4579 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4579 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2492 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    u. cun 3310   {csn 3806   suc csuc 4575
This theorem is referenced by:  eqelsuc  4654  suc11  4677  ordunisuc  4804  onsucuni2  4806  onuninsuci  4812  limsuc  4821  tfindes  4834  tfinds2  4835  findes  4867  onnseq  6598  seqomlem0  6698  seqomlem1  6699  seqomlem4  6702  oasuc  6760  onasuc  6764  oa1suc  6767  oa0r  6774  oaass  6796  oneo  6816  omeulem1  6817  oeeulem  6836  oeeui  6837  nna0r  6844  nnacom  6852  nnaass  6857  nnmsucr  6860  omabs  6882  nnneo  6886  nneob  6887  omsmolem  6888  omopthlem1  6890  limensuc  7276  infensuc  7277  nneneq  7282  unblem2  7352  unblem3  7353  suc11reg  7566  inf0  7568  inf3lem1  7575  dfom3  7594  cantnflt  7619  cantnflem1  7637  cnfcom  7649  r1elwf  7714  rankidb  7718  rankonidlem  7746  ranklim  7762  rankopb  7770  rankelop  7792  rankxpu  7794  rankxplim  7795  cardsucnn  7864  dif1card  7884  infxpenlem  7887  fseqenlem1  7897  dfac12lem1  8015  dfac12lem2  8016  dfac12r  8018  pwsdompw  8076  ackbij1lem5  8096  ackbij1lem14  8105  ackbij1lem18  8109  ackbij1  8110  ackbij2lem3  8113  cfsmolem  8142  cfsmo  8143  sornom  8149  isfin3ds  8201  isf32lem1  8225  isf32lem2  8226  isf32lem5  8229  isf32lem6  8230  isf32lem7  8231  isf32lem8  8232  isf32lem11  8235  fin1a2lem1  8272  ituniiun  8294  axdc2lem  8320  axdc3lem2  8323  axdc3lem3  8324  axdc3lem4  8325  axdc3  8326  axdc4lem  8327  axcclem  8329  axdclem2  8392  wunex2  8605  om2uzsuci  11280  axdc4uzlem  11313  nofulllem1  25649  nofulllem2  25650  rankaltopb  25816  ranksng  26100  rankpwg  26102  rankeq1o  26104  ontgsucval  26174  onsuccon  26180  onsucsuccmp  26186  limsucncmp  26188  ordcmp  26189  limsuc2  27106  aomclem4  27123  aomclem8  27127  bnj222  29191  bnj966  29252  bnj1112  29289
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-sn 3812  df-suc 4579
  Copyright terms: Public domain W3C validator