Theorem suceq 6335

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 4572	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4099	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6276	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6276	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3886  {csn 4562  suc csuc 6272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-sn 4563  df-suc 6276

This theorem is referenced by:  eqelsuc  6351  suc11  6373  ordunisuc  7688  onsucuni2  7690  onuninsuci  7696  limsuc  7705  tfindes  7718  tfinds2  7719  peano5  7749  findes  7758  onnseq  8184  seqomlem0  8289  seqomlem1  8290  seqomlem4  8293  oasuc  8363  onasuc  8367  oa1suc  8370  oa0r  8377  o2p2e4  8380  o2p2e4OLD  8381  oaass  8401  oneo  8421  omeulem1  8422  oeeulem  8441  oeeui  8442  nna0r  8449  nnacom  8457  nnaass  8462  nnmsucr  8465  omabs  8490  nnneo  8494  nneob  8495  omsmolem  8496  omopthlem1  8498  eldifsucnn  8503  limensuc  8950  infensuc  8951  nneneq  9001  nneneqOLD  9013  unblem2  9076  unblem3  9077  suc11reg  9386  inf0  9388  inf3lem1  9395  dfom3  9414  cantnflt  9439  cantnflem1  9456  cnfcom  9467  brttrcl2  9481  ssttrcl  9482  ttrcltr  9483  ttrclss  9487  dmttrcl  9488  rnttrcl  9489  ttrclselem2  9493  r1elwf  9563  rankidb  9567  rankonidlem  9595  ranklim  9611  rankopb  9619  rankelop  9641  rankxpu  9643  rankmapu  9645  rankxplim  9646  cardsucnn  9752  dif1card  9775  infxpenlem  9778  fseqenlem1  9789  dfac12lem1  9908  dfac12lem2  9909  dfac12r  9911  pwsdompw  9969  ackbij1lem14  9998  ackbij1lem18  10002  ackbij1  10003  ackbij2lem3  10006  cfsmolem  10035  cfsmo  10036  sornom  10042  isfin3ds  10094  isf32lem1  10118  isf32lem2  10119  isf32lem5  10122  isf32lem6  10123  isf32lem7  10124  isf32lem8  10125  isf32lem11  10128  fin1a2lem1  10165  ituniiun  10187  axdc2lem  10213  axdc3lem2  10216  axdc3lem3  10217  axdc3lem4  10218  axdc3  10219  axdc4lem  10220  axcclem  10222  axdclem2  10285  wunex2  10503  om2uzsuci  13677  axdc4uzlem  13712  bnj222  32872  bnj966  32933  bnj1112  32972  gonar  33366  goalr  33368  satffun  33380  noresle  33909  nosupcbv  33914  nosupno  33915  nosupdm  33916  nosupfv  33918  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem3  33922  nosupbnd1lem5  33924  nosupbnd2  33928  noinfcbv  33929  noinfno  33930  noinfdm  33931  noinffv  33933  noinfres  33934  noinfbnd1lem3  33937  noinfbnd1lem5  33939  bday1s  34034  rankaltopb  34290  ranksng  34478  rankpwg  34480  rankeq1o  34482  ontgsucval  34630  onsucconn  34636  onsucsuccmp  34642  limsucncmp  34644  ordcmp  34645  finxpreclem4  35574  finxp00  35582  limsuc2  40873  aomclem4  40889  aomclem8  40893  suceqd  41829  onsetreclem1  46421