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  6507  tfrcllemsucaccv  6520  tfrcl  6530  frecabcl  6565  frecsuc  6573  sucinc  6613  sucinc2  6614  oacl  6628  oav2  6631  oasuc  6632  oa1suc  6635  nna0r  6646  nnacom  6652  nnaass  6653  nnmsucr  6656  nnsucelsuc  6659  nnsucsssuc  6660  nnaword  6679  nnaordex  6696  phplem3g  7042  nneneq  7043  php5  7044  php5dom  7049  omp1eomlem  7293  omp1eom  7294  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  nninfwlpoim  7378  nninfinfwlpo  7379  indpi  7562  ennnfoneleminc  13050  ennnfonelemex  13053  bj-indsuc  16574  bj-bdfindes  16595  bj-nn0suc0  16596  bj-peano4  16601  bj-inf2vnlem1  16616  bj-nn0sucALT  16624  bj-findes  16627  nnsf  16658  nninfsellemdc  16663  nninfself  16666  nninfsellemeqinf  16669  nninfomni  16672