Theorem suceq 4448

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 3643	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3327	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4417	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4417	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2262	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1372   ∪ cun 3163  {csn 3632  suc csuc 4411

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-suc 4417

This theorem is referenced by:  eqelsuc  4465  2ordpr  4571  onsucsssucexmid  4574  onsucelsucexmid  4577  ordsucunielexmid  4578  suc11g  4604  onsucuni2  4611  0elsucexmid  4612  ordpwsucexmid  4617  peano2  4642  findes  4650  nn0suc  4651  0elnn  4666  omsinds  4669  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  tfrcl  6449  frecabcl  6484  frecsuc  6492  sucinc  6530  sucinc2  6531  oacl  6545  oav2  6548  oasuc  6549  oa1suc  6552  nna0r  6563  nnacom  6569  nnaass  6570  nnmsucr  6573  nnsucelsuc  6576  nnsucsssuc  6577  nnaword  6596  nnaordex  6613  phplem3g  6952  nneneq  6953  php5  6954  php5dom  6959  omp1eomlem  7195  omp1eom  7196  nninfninc  7224  nnnninfeq  7229  nnnninfeq2  7230  nninfwlpoimlemg  7276  nninfwlpoimlemginf  7277  nninfwlpoim  7280  nninfinfwlpo  7281  indpi  7454  ennnfoneleminc  12753  ennnfonelemex  12756  bj-indsuc  15826  bj-bdfindes  15847  bj-nn0suc0  15848  bj-peano4  15853  bj-inf2vnlem1  15868  bj-nn0sucALT  15876  bj-findes  15879  nnsf  15904  nninfsellemdc  15909  nninfself  15912  nninfsellemeqinf  15915  nninfomni  15918