Theorem suceq 6428

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 4638	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4164	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6368	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6368	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3946  {csn 4628  suc csuc 6364

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-sn 4629  df-suc 6368

This theorem is referenced by:  eqelsuc  6446  suc11  6469  ordunisuc  7817  onsucuni2  7819  onuninsuci  7826  limsuc  7835  tfindes  7849  tfinds2  7850  peano5  7881  findes  7890  onnseq  8341  seqomlem0  8446  seqomlem1  8447  seqomlem4  8450  oasuc  8521  onasuc  8525  oa1suc  8528  oa0r  8535  o2p2e4  8538  oaass  8558  oneo  8578  omeulem1  8579  oeeulem  8598  oeeui  8599  nna0r  8606  nnacom  8614  nnaass  8619  nnmsucr  8622  omabs  8647  nnneo  8651  nneob  8652  omsmolem  8653  omopthlem1  8655  eldifsucnn  8660  limensuc  9151  infensuc  9152  nneneq  9206  nneneqOLD  9218  unblem2  9293  unblem3  9294  suc11reg  9611  inf0  9613  inf3lem1  9620  dfom3  9639  cantnflt  9664  cantnflem1  9681  cnfcom  9692  brttrcl2  9706  ssttrcl  9707  ttrcltr  9708  ttrclss  9712  dmttrcl  9713  rnttrcl  9714  ttrclselem2  9718  r1elwf  9788  rankidb  9792  rankonidlem  9820  ranklim  9836  rankopb  9844  rankelop  9866  rankxpu  9868  rankmapu  9870  rankxplim  9871  cardsucnn  9977  dif1card  10002  infxpenlem  10005  fseqenlem1  10016  dfac12lem1  10135  dfac12lem2  10136  dfac12r  10138  pwsdompw  10196  ackbij1lem14  10225  ackbij1lem18  10229  ackbij1  10230  ackbij2lem3  10233  cfsmolem  10262  cfsmo  10263  sornom  10269  isfin3ds  10321  isf32lem1  10345  isf32lem2  10346  isf32lem5  10349  isf32lem6  10350  isf32lem7  10351  isf32lem8  10352  isf32lem11  10355  fin1a2lem1  10392  ituniiun  10414  axdc2lem  10440  axdc3lem2  10443  axdc3lem3  10444  axdc3lem4  10445  axdc3  10446  axdc4lem  10447  axcclem  10449  axdclem2  10512  wunex2  10730  om2uzsuci  13910  axdc4uzlem  13945  noresle  27190  nosupcbv  27195  nosupno  27196  nosupdm  27197  nosupfv  27199  nosupres  27200  nosupbnd1lem1  27201  nosupbnd1lem3  27203  nosupbnd1lem5  27205  nosupbnd2  27209  noinfcbv  27210  noinfno  27211  noinfdm  27212  noinffv  27214  noinfres  27215  noinfbnd1lem3  27218  noinfbnd1lem5  27220  bday1s  27322  bnj222  33883  bnj966  33944  bnj1112  33983  gonar  34375  goalr  34377  satffun  34389  rankaltopb  34940  ranksng  35128  rankpwg  35130  rankeq1o  35132  ontgsucval  35306  onsucconn  35312  onsucsuccmp  35318  limsucncmp  35320  ordcmp  35321  finxpreclem4  36264  finxp00  36272  limsuc2  41769  aomclem4  41785  aomclem8  41789  onsucelab  41999  onsucf1olem  42006  onsucrn  42007  onov0suclim  42010  onsucunifi  42106  sucunisn  42107  onsucunipr  42108  onsucunitp  42109  nadd1suc  42128  naddsuc2  42129  naddonnn  42132  suceqd  42949  onsetreclem1  47704