Theorem suceq 6003

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 4380	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3967	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 5942	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 5942	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2865	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1637   ∪ cun 3767  {csn 4370  suc csuc 5938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-un 3774  df-sn 4371  df-suc 5942

This theorem is referenced by:  eqelsuc  6019  suc11  6044  ordunisuc  7262  onsucuni2  7264  onuninsuci  7270  limsuc  7279  tfindes  7292  tfinds2  7293  findes  7326  onnseq  7677  seqomlem0  7780  seqomlem1  7781  seqomlem4  7784  oasuc  7841  onasuc  7845  oa1suc  7848  oa0r  7855  o2p2e4  7858  oaass  7878  oneo  7898  omeulem1  7899  oeeulem  7918  oeeui  7919  nna0r  7926  nnacom  7934  nnaass  7939  nnmsucr  7942  omabs  7964  nnneo  7968  nneob  7969  omsmolem  7970  omopthlem1  7972  limensuc  8376  infensuc  8377  nneneq  8382  unblem2  8452  unblem3  8453  suc11reg  8763  inf0  8765  inf3lem1  8772  dfom3  8791  cantnflt  8816  cantnflem1  8833  cnfcom  8844  r1elwf  8906  rankidb  8910  rankonidlem  8938  ranklim  8954  rankopb  8962  rankelop  8984  rankxpu  8986  rankmapu  8988  rankxplim  8989  cardsucnn  9094  dif1card  9116  infxpenlem  9119  fseqenlem1  9130  dfac12lem1  9250  dfac12lem2  9251  dfac12r  9253  pwsdompw  9311  ackbij1lem14  9340  ackbij1lem18  9344  ackbij1  9345  ackbij2lem3  9348  cfsmolem  9377  cfsmo  9378  sornom  9384  isfin3ds  9436  isf32lem1  9460  isf32lem2  9461  isf32lem5  9464  isf32lem6  9465  isf32lem7  9466  isf32lem8  9467  isf32lem11  9470  fin1a2lem1  9507  ituniiun  9529  axdc2lem  9555  axdc3lem2  9558  axdc3lem3  9559  axdc3lem4  9560  axdc3  9561  axdc4lem  9562  axcclem  9564  axdclem2  9627  wunex2  9845  om2uzsuci  12971  axdc4uzlem  13006  bnj222  31276  bnj966  31337  bnj1112  31374  noresle  32167  nosupno  32170  nosupdm  32171  nosupfv  32173  nosupres  32174  nosupbnd1lem1  32175  nosupbnd1lem3  32177  nosupbnd1lem5  32179  nosupbnd2  32183  noetalem4  32187  noeta  32189  rankaltopb  32407  ranksng  32595  rankpwg  32597  rankeq1o  32599  ontgsucval  32748  onsucconn  32754  onsucsuccmp  32760  limsucncmp  32762  ordcmp  32763  finxpreclem4  33547  finxp00  33555  limsuc2  38112  aomclem4  38128  aomclem8  38132  onsetreclem1  43019