Theorem suceq 6419

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

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		sneq 4611	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4144	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6358	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6358	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2795	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3924  {csn 4601  suc csuc 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-suc 6358

This theorem is referenced by:  eqelsuc  6437  suc11  6460  ordunisuc  7824  onsucuni2  7826  onuninsuci  7833  limsuc  7842  tfindes  7856  tfinds2  7857  peano5  7887  findes  7894  onnseq  8356  seqomlem0  8461  seqomlem1  8462  seqomlem4  8465  oasuc  8534  onasuc  8538  oa1suc  8541  oa0r  8548  o2p2e4  8551  oaass  8571  oneo  8591  omeulem1  8592  oeeulem  8611  oeeui  8612  nna0r  8619  nnacom  8627  nnaass  8632  nnmsucr  8635  omabs  8661  nnneo  8665  nneob  8666  omsmolem  8667  omopthlem1  8669  eldifsucnn  8674  naddsuc2  8711  naddoa  8712  limensuc  9166  infensuc  9167  nneneq  9218  unblem2  9299  unblem3  9300  suc11reg  9631  inf0  9633  inf3lem1  9640  dfom3  9659  cantnflt  9684  cantnflem1  9701  cnfcom  9712  brttrcl2  9726  ssttrcl  9727  ttrcltr  9728  ttrclss  9732  dmttrcl  9733  rnttrcl  9734  ttrclselem2  9738  r1elwf  9808  rankidb  9812  rankonidlem  9840  ranklim  9856  rankopb  9864  rankelop  9886  rankxpu  9888  rankmapu  9890  rankxplim  9891  cardsucnn  9997  dif1card  10022  infxpenlem  10025  fseqenlem1  10036  dfac12lem1  10156  dfac12lem2  10157  dfac12r  10159  pwsdompw  10215  ackbij1lem14  10244  ackbij1lem18  10248  ackbij1  10249  ackbij2lem3  10252  cfsmolem  10282  cfsmo  10283  sornom  10289  isfin3ds  10341  isf32lem1  10365  isf32lem2  10366  isf32lem5  10369  isf32lem6  10370  isf32lem7  10371  isf32lem8  10372  isf32lem11  10375  fin1a2lem1  10412  ituniiun  10434  axdc2lem  10460  axdc3lem2  10463  axdc3lem3  10464  axdc3lem4  10465  axdc3  10466  axdc4lem  10467  axcclem  10469  axdclem2  10532  wunex2  10750  om2uzsuci  13964  axdc4uzlem  13999  noresle  27659  nosupcbv  27664  nosupno  27665  nosupdm  27666  nosupfv  27668  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1lem3  27672  nosupbnd1lem5  27674  nosupbnd2  27678  noinfcbv  27679  noinfno  27680  noinfdm  27681  noinffv  27683  noinfres  27684  noinfbnd1lem3  27687  noinfbnd1lem5  27689  bday1s  27793  om2noseqlt  28222  bnj222  34860  bnj966  34921  bnj1112  34960  gonar  35363  goalr  35365  satffun  35377  rankaltopb  35943  ranksng  36131  rankpwg  36133  rankeq1o  36135  ontgsucval  36396  onsucconn  36402  onsucsuccmp  36408  limsucncmp  36410  ordcmp  36411  finxpreclem4  37358  finxp00  37366  limsuc2  43012  aomclem4  43028  aomclem8  43032  onsucelab  43234  onsucf1olem  43241  onsucrn  43242  onov0suclim  43245  onsucunifi  43341  sucunisn  43342  onsucunipr  43343  onsucunitp  43344  nadd1suc  43363  naddonnn  43366  suceqd  44181  onsetreclem1  49517