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

Theorem suceq 5933
 Description: Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
suceq (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Proof of Theorem suceq
StepHypRef Expression
1 id 22 . . 3 (𝐴 = 𝐵𝐴 = 𝐵)
2 sneq 4324 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2uneq12d 3917 . 2 (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4 df-suc 5872 . 2 suc 𝐴 = (𝐴 ∪ {𝐴})
5 df-suc 5872 . 2 suc 𝐵 = (𝐵 ∪ {𝐵})
63, 4, 53eqtr4g 2829 1 (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1630   ∪ cun 3719  {csn 4314  suc csuc 5868 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-un 3726  df-sn 4315  df-suc 5872 This theorem is referenced by:  eqelsuc  5949  suc11  5974  ordunisuc  7178  onsucuni2  7180  onuninsuci  7186  limsuc  7195  tfindes  7208  tfinds2  7209  findes  7242  onnseq  7593  seqomlem0  7696  seqomlem1  7697  seqomlem4  7700  oasuc  7757  onasuc  7761  oa1suc  7764  oa0r  7771  o2p2e4  7774  oaass  7794  oneo  7814  omeulem1  7815  oeeulem  7834  oeeui  7835  nna0r  7842  nnacom  7850  nnaass  7855  nnmsucr  7858  omabs  7880  nnneo  7884  nneob  7885  omsmolem  7886  omopthlem1  7888  limensuc  8292  infensuc  8293  nneneq  8298  unblem2  8368  unblem3  8369  suc11reg  8679  inf0  8681  inf3lem1  8688  dfom3  8707  cantnflt  8732  cantnflem1  8749  cnfcom  8760  r1elwf  8822  rankidb  8826  rankonidlem  8854  ranklim  8870  rankopb  8878  rankelop  8900  rankxpu  8902  rankmapu  8904  rankxplim  8905  cardsucnn  9010  dif1card  9032  infxpenlem  9035  fseqenlem1  9046  dfac12lem1  9166  dfac12lem2  9167  dfac12r  9169  pwsdompw  9227  ackbij1lem14  9256  ackbij1lem18  9260  ackbij1  9261  ackbij2lem3  9264  cfsmolem  9293  cfsmo  9294  sornom  9300  isfin3ds  9352  isf32lem1  9376  isf32lem2  9377  isf32lem5  9380  isf32lem6  9381  isf32lem7  9382  isf32lem8  9383  isf32lem11  9386  fin1a2lem1  9423  ituniiun  9445  axdc2lem  9471  axdc3lem2  9474  axdc3lem3  9475  axdc3lem4  9476  axdc3  9477  axdc4lem  9478  axcclem  9480  axdclem2  9543  wunex2  9761  om2uzsuci  12954  axdc4uzlem  12989  bnj222  31285  bnj966  31346  bnj1112  31383  noresle  32177  nosupno  32180  nosupdm  32181  nosupfv  32183  nosupres  32184  nosupbnd1lem1  32185  nosupbnd1lem3  32187  nosupbnd1lem5  32189  nosupbnd2  32193  noetalem4  32197  noeta  32199  rankaltopb  32417  ranksng  32605  rankpwg  32607  rankeq1o  32609  ontgsucval  32762  onsucconn  32768  onsucsuccmp  32774  limsucncmp  32776  ordcmp  32777  finxpreclem4  33561  finxp00  33569  limsuc2  38130  aomclem4  38146  aomclem8  38150  onsetreclem1  42969
 Copyright terms: Public domain W3C validator