Theorem suceq 4523

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 19	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		sneq 3700	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3374	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4492	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4492	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2290	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1398   ∪ cun 3209  {csn 3689  suc csuc 4486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-suc 4492

This theorem is referenced by:  eqelsuc  4540  2ordpr  4646  onsucsssucexmid  4649  onsucelsucexmid  4652  ordsucunielexmid  4653  suc11g  4679  onsucuni2  4686  0elsucexmid  4687  ordpwsucexmid  4692  peano2  4717  findes  4725  nn0suc  4726  0elnn  4741  omsinds  4744  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  tfrcl  6595  frecabcl  6630  frecsuc  6638  sucinc  6678  sucinc2  6679  oacl  6693  oav2  6696  oasuc  6697  oa1suc  6700  nna0r  6711  nnacom  6717  nnaass  6718  nnmsucr  6721  nnsucelsuc  6724  nnsucsssuc  6725  nnaword  6744  nnaordex  6761  phplem3g  7110  nneneq  7111  php5  7112  php5dom  7117  omp1eomlem  7385  omp1eom  7386  nninfninc  7414  nnnninfeq  7419  nnnninfeq2  7420  nninfwlpoimlemg  7466  nninfwlpoimlemginf  7467  nninfwlpoim  7470  nninfinfwlpo  7471  indpi  7657  ennnfoneleminc  13162  ennnfonelemex  13165  bj-indsuc  16698  bj-bdfindes  16719  bj-nn0suc0  16720  bj-peano4  16725  bj-inf2vnlem1  16740  bj-nn0sucALT  16748  bj-findes  16751  nnsf  16783  nninfsellemdc  16788  nninfself  16791  nninfsellemeqinf  16794  nninfomni  16797