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

Theorem suceq 5475
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 3982 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3598 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 5416 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 5416 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2468 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    u. cun 3412   {csn 3972   suc csuc 5412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-un 3419  df-sn 3973  df-suc 5416
This theorem is referenced by:  eqelsuc  5491  suc11  5513  ordunisuc  6650  onsucuni2  6652  onuninsuci  6658  limsuc  6667  tfindes  6680  tfinds2  6681  findes  6714  onnseq  7048  seqomlem0  7151  seqomlem1  7152  seqomlem4  7155  oasuc  7211  onasuc  7215  oa1suc  7218  oa0r  7225  oaass  7247  oneo  7267  omeulem1  7268  oeeulem  7287  oeeui  7288  nna0r  7295  nnacom  7303  nnaass  7308  nnmsucr  7311  omabs  7333  nnneo  7337  nneob  7338  omsmolem  7339  omopthlem1  7341  limensuc  7732  infensuc  7733  nneneq  7738  unblem2  7807  unblem3  7808  suc11reg  8069  inf0  8071  inf3lem1  8078  dfom3  8097  cantnflt  8123  cantnflem1  8140  cantnfltOLD  8153  cantnflem1OLD  8163  cnfcom  8176  cnfcomOLD  8184  r1elwf  8246  rankidb  8250  rankonidlem  8278  ranklim  8294  rankopb  8302  rankelop  8324  rankxpu  8326  rankmapu  8328  rankxplim  8329  cardsucnn  8398  dif1card  8420  infxpenlem  8423  fseqenlem1  8437  dfac12lem1  8555  dfac12lem2  8556  dfac12r  8558  pwsdompw  8616  ackbij1lem5  8636  ackbij1lem14  8645  ackbij1lem18  8649  ackbij1  8650  ackbij2lem3  8653  cfsmolem  8682  cfsmo  8683  sornom  8689  isfin3ds  8741  isf32lem1  8765  isf32lem2  8766  isf32lem5  8769  isf32lem6  8770  isf32lem7  8771  isf32lem8  8772  isf32lem11  8775  fin1a2lem1  8812  ituniiun  8834  axdc2lem  8860  axdc3lem2  8863  axdc3lem3  8864  axdc3lem4  8865  axdc3  8866  axdc4lem  8867  axcclem  8869  axdclem2  8932  wunex2  9146  om2uzsuci  12100  axdc4uzlem  12133  bnj222  29268  bnj966  29329  bnj1112  29366  nofulllem1  30162  nofulllem2  30163  rankaltopb  30317  ranksng  30505  rankpwg  30507  rankeq1o  30509  ontgsucval  30664  onsuccon  30670  onsucsuccmp  30676  limsucncmp  30678  ordcmp  30679  limsuc2  35348  aomclem4  35365  aomclem8  35369
  Copyright terms: Public domain W3C validator