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

Theorem suceq 4936
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 4030 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3652 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4877 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4877 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2526 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    u. cun 3467   {csn 4020   suc csuc 4873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474  df-sn 4021  df-suc 4877
This theorem is referenced by:  eqelsuc  4952  suc11  4974  ordunisuc  6638  onsucuni2  6640  onuninsuci  6646  limsuc  6655  tfindes  6668  tfinds2  6669  findes  6701  onnseq  7005  seqomlem0  7104  seqomlem1  7105  seqomlem4  7108  oasuc  7164  onasuc  7168  oa1suc  7171  oa0r  7178  oaass  7200  oneo  7220  omeulem1  7221  oeeulem  7240  oeeui  7241  nna0r  7248  nnacom  7256  nnaass  7261  nnmsucr  7264  omabs  7286  nnneo  7290  nneob  7291  omsmolem  7292  omopthlem1  7294  limensuc  7684  infensuc  7685  nneneq  7690  unblem2  7762  unblem3  7763  suc11reg  8025  inf0  8027  inf3lem1  8034  dfom3  8053  cantnflt  8080  cantnflem1  8097  cantnfltOLD  8110  cantnflem1OLD  8120  cnfcom  8133  cnfcomOLD  8141  r1elwf  8203  rankidb  8207  rankonidlem  8235  ranklim  8251  rankopb  8259  rankelop  8281  rankxpu  8283  rankmapu  8285  rankxplim  8286  cardsucnn  8355  dif1card  8377  infxpenlem  8380  fseqenlem1  8394  dfac12lem1  8512  dfac12lem2  8513  dfac12r  8515  pwsdompw  8573  ackbij1lem5  8593  ackbij1lem14  8602  ackbij1lem18  8606  ackbij1  8607  ackbij2lem3  8610  cfsmolem  8639  cfsmo  8640  sornom  8646  isfin3ds  8698  isf32lem1  8722  isf32lem2  8723  isf32lem5  8726  isf32lem6  8727  isf32lem7  8728  isf32lem8  8729  isf32lem11  8732  fin1a2lem1  8769  ituniiun  8791  axdc2lem  8817  axdc3lem2  8820  axdc3lem3  8821  axdc3lem4  8822  axdc3  8823  axdc4lem  8824  axcclem  8826  axdclem2  8889  wunex2  9105  om2uzsuci  12015  axdc4uzlem  12048  nofulllem1  28889  nofulllem2  28890  rankaltopb  29056  ranksng  29251  rankpwg  29253  rankeq1o  29255  ontgsucval  29324  onsuccon  29330  onsucsuccmp  29336  limsucncmp  29338  ordcmp  29339  limsuc2  30443  aomclem4  30460  aomclem8  30464  bnj222  32895  bnj966  32956  bnj1112  32993
  Copyright terms: Public domain W3C validator