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

Theorem suceq 4884
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 3987 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3611 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4825 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4825 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2517 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    u. cun 3426   {csn 3977   suc csuc 4821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-un 3433  df-sn 3978  df-suc 4825
This theorem is referenced by:  eqelsuc  4900  suc11  4922  ordunisuc  6545  onsucuni2  6547  onuninsuci  6553  limsuc  6562  tfindes  6575  tfinds2  6576  findes  6608  onnseq  6907  seqomlem0  7006  seqomlem1  7007  seqomlem4  7010  oasuc  7066  onasuc  7070  oa1suc  7073  oa0r  7080  oaass  7102  oneo  7122  omeulem1  7123  oeeulem  7142  oeeui  7143  nna0r  7150  nnacom  7158  nnaass  7163  nnmsucr  7166  omabs  7188  nnneo  7192  nneob  7193  omsmolem  7194  omopthlem1  7196  limensuc  7590  infensuc  7591  nneneq  7596  unblem2  7668  unblem3  7669  suc11reg  7928  inf0  7930  inf3lem1  7937  dfom3  7956  cantnflt  7983  cantnflem1  8000  cantnfltOLD  8013  cantnflem1OLD  8023  cnfcom  8036  cnfcomOLD  8044  r1elwf  8106  rankidb  8110  rankonidlem  8138  ranklim  8154  rankopb  8162  rankelop  8184  rankxpu  8186  rankmapu  8188  rankxplim  8189  cardsucnn  8258  dif1card  8280  infxpenlem  8283  fseqenlem1  8297  dfac12lem1  8415  dfac12lem2  8416  dfac12r  8418  pwsdompw  8476  ackbij1lem5  8496  ackbij1lem14  8505  ackbij1lem18  8509  ackbij1  8510  ackbij2lem3  8513  cfsmolem  8542  cfsmo  8543  sornom  8549  isfin3ds  8601  isf32lem1  8625  isf32lem2  8626  isf32lem5  8629  isf32lem6  8630  isf32lem7  8631  isf32lem8  8632  isf32lem11  8635  fin1a2lem1  8672  ituniiun  8694  axdc2lem  8720  axdc3lem2  8723  axdc3lem3  8724  axdc3lem4  8725  axdc3  8726  axdc4lem  8727  axcclem  8729  axdclem2  8792  wunex2  9008  om2uzsuci  11874  axdc4uzlem  11907  nofulllem1  27979  nofulllem2  27980  rankaltopb  28146  ranksng  28341  rankpwg  28343  rankeq1o  28345  ontgsucval  28414  onsuccon  28420  onsucsuccmp  28426  limsucncmp  28428  ordcmp  28429  limsuc2  29533  aomclem4  29550  aomclem8  29554  bnj222  32178  bnj966  32239  bnj1112  32276
  Copyright terms: Public domain W3C validator