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

Theorem suceq 4779
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 3882 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3506 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4720 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4720 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2495 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    u. cun 3321   {csn 3872   suc csuc 4716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-sn 3873  df-suc 4720
This theorem is referenced by:  eqelsuc  4795  suc11  4817  ordunisuc  6438  onsucuni2  6440  onuninsuci  6446  limsuc  6455  tfindes  6468  tfinds2  6469  findes  6501  onnseq  6797  seqomlem0  6896  seqomlem1  6897  seqomlem4  6900  oasuc  6956  onasuc  6960  oa1suc  6963  oa0r  6970  oaass  6992  oneo  7012  omeulem1  7013  oeeulem  7032  oeeui  7033  nna0r  7040  nnacom  7048  nnaass  7053  nnmsucr  7056  omabs  7078  nnneo  7082  nneob  7083  omsmolem  7084  omopthlem1  7086  limensuc  7480  infensuc  7481  nneneq  7486  unblem2  7557  unblem3  7558  suc11reg  7817  inf0  7819  inf3lem1  7826  dfom3  7845  cantnflt  7872  cantnflem1  7889  cantnfltOLD  7902  cantnflem1OLD  7912  cnfcom  7925  cnfcomOLD  7933  r1elwf  7995  rankidb  7999  rankonidlem  8027  ranklim  8043  rankopb  8051  rankelop  8073  rankxpu  8075  rankmapu  8077  rankxplim  8078  cardsucnn  8147  dif1card  8169  infxpenlem  8172  fseqenlem1  8186  dfac12lem1  8304  dfac12lem2  8305  dfac12r  8307  pwsdompw  8365  ackbij1lem5  8385  ackbij1lem14  8394  ackbij1lem18  8398  ackbij1  8399  ackbij2lem3  8402  cfsmolem  8431  cfsmo  8432  sornom  8438  isfin3ds  8490  isf32lem1  8514  isf32lem2  8515  isf32lem5  8518  isf32lem6  8519  isf32lem7  8520  isf32lem8  8521  isf32lem11  8524  fin1a2lem1  8561  ituniiun  8583  axdc2lem  8609  axdc3lem2  8612  axdc3lem3  8613  axdc3lem4  8614  axdc3  8615  axdc4lem  8616  axcclem  8618  axdclem2  8681  wunex2  8897  om2uzsuci  11763  axdc4uzlem  11796  nofulllem1  27812  nofulllem2  27813  rankaltopb  27979  ranksng  28174  rankpwg  28176  rankeq1o  28178  ontgsucval  28248  onsuccon  28254  onsucsuccmp  28260  limsucncmp  28262  ordcmp  28263  limsuc2  29364  aomclem4  29381  aomclem8  29385  bnj222  31805  bnj966  31866  bnj1112  31903
  Copyright terms: Public domain W3C validator