Theorem suceq 6094

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 4451	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4030	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6035	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6035	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2840	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1507   ∪ cun 3828  {csn 4441  suc csuc 6031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-v 3418  df-un 3835  df-sn 4442  df-suc 6035

This theorem is referenced by:  eqelsuc  6110  suc11  6132  ordunisuc  7363  onsucuni2  7365  onuninsuci  7371  limsuc  7380  tfindes  7393  tfinds2  7394  findes  7427  onnseq  7785  seqomlem0  7888  seqomlem1  7889  seqomlem4  7892  oasuc  7951  onasuc  7955  oa1suc  7958  oa0r  7965  o2p2e4  7968  oaass  7988  oneo  8008  omeulem1  8009  oeeulem  8028  oeeui  8029  nna0r  8036  nnacom  8044  nnaass  8049  nnmsucr  8052  omabs  8074  nnneo  8078  nneob  8079  omsmolem  8080  omopthlem1  8082  limensuc  8490  infensuc  8491  nneneq  8496  unblem2  8566  unblem3  8567  suc11reg  8876  inf0  8878  inf3lem1  8885  dfom3  8904  cantnflt  8929  cantnflem1  8946  cnfcom  8957  r1elwf  9019  rankidb  9023  rankonidlem  9051  ranklim  9067  rankopb  9075  rankelop  9097  rankxpu  9099  rankmapu  9101  rankxplim  9102  cardsucnn  9208  dif1card  9230  infxpenlem  9233  fseqenlem1  9244  dfac12lem1  9363  dfac12lem2  9364  dfac12r  9366  pwsdompw  9424  ackbij1lem14  9453  ackbij1lem18  9457  ackbij1  9458  ackbij2lem3  9461  cfsmolem  9490  cfsmo  9491  sornom  9497  isfin3ds  9549  isf32lem1  9573  isf32lem2  9574  isf32lem5  9577  isf32lem6  9578  isf32lem7  9579  isf32lem8  9580  isf32lem11  9583  fin1a2lem1  9620  ituniiun  9642  axdc2lem  9668  axdc3lem2  9671  axdc3lem3  9672  axdc3lem4  9673  axdc3  9674  axdc4lem  9675  axcclem  9677  axdclem2  9740  wunex2  9958  om2uzsuci  13131  axdc4uzlem  13166  bnj222  31799  bnj966  31860  bnj1112  31897  noresle  32718  nosupno  32721  nosupdm  32722  nosupfv  32724  nosupres  32725  nosupbnd1lem1  32726  nosupbnd1lem3  32728  nosupbnd1lem5  32730  nosupbnd2  32734  noetalem4  32738  noeta  32740  rankaltopb  32958  ranksng  33146  rankpwg  33148  rankeq1o  33150  ontgsucval  33297  onsucconn  33303  onsucsuccmp  33309  limsucncmp  33311  ordcmp  33312  finxpreclem4  34113  finxp00  34121  limsuc2  39034  aomclem4  39050  aomclem8  39054  suceqd  39935  onsetreclem1  44172