Theorem suceq 4499

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 3680	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3362	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4468	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4468	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2289	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1397   ∪ cun 3198  {csn 3669  suc csuc 4462

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-suc 4468

This theorem is referenced by:  eqelsuc  4516  2ordpr  4622  onsucsssucexmid  4625  onsucelsucexmid  4628  ordsucunielexmid  4629  suc11g  4655  onsucuni2  4662  0elsucexmid  4663  ordpwsucexmid  4668  peano2  4693  findes  4701  nn0suc  4702  0elnn  4717  omsinds  4720  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  tfrcl  6529  frecabcl  6564  frecsuc  6572  sucinc  6612  sucinc2  6613  oacl  6627  oav2  6630  oasuc  6631  oa1suc  6634  nna0r  6645  nnacom  6651  nnaass  6652  nnmsucr  6655  nnsucelsuc  6658  nnsucsssuc  6659  nnaword  6678  nnaordex  6695  phplem3g  7041  nneneq  7042  php5  7043  php5dom  7048  omp1eomlem  7292  omp1eom  7293  nninfninc  7321  nnnninfeq  7326  nnnninfeq2  7327  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  nninfwlpoim  7377  nninfinfwlpo  7378  indpi  7561  ennnfoneleminc  13031  ennnfonelemex  13034  bj-indsuc  16523  bj-bdfindes  16544  bj-nn0suc0  16545  bj-peano4  16550  bj-inf2vnlem1  16565  bj-nn0sucALT  16573  bj-findes  16576  nnsf  16607  nninfsellemdc  16612  nninfself  16615  nninfsellemeqinf  16618  nninfomni  16621