Theorem suceq 4492

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 3677	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3359	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4461	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4461	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1395   ∪ cun 3195  {csn 3666  suc csuc 4455

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-suc 4461

This theorem is referenced by:  eqelsuc  4509  2ordpr  4615  onsucsssucexmid  4618  onsucelsucexmid  4621  ordsucunielexmid  4622  suc11g  4648  onsucuni2  4655  0elsucexmid  4656  ordpwsucexmid  4661  peano2  4686  findes  4694  nn0suc  4695  0elnn  4710  omsinds  4713  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  tfrcl  6508  frecabcl  6543  frecsuc  6551  sucinc  6589  sucinc2  6590  oacl  6604  oav2  6607  oasuc  6608  oa1suc  6611  nna0r  6622  nnacom  6628  nnaass  6629  nnmsucr  6632  nnsucelsuc  6635  nnsucsssuc  6636  nnaword  6655  nnaordex  6672  phplem3g  7013  nneneq  7014  php5  7015  php5dom  7020  omp1eomlem  7257  omp1eom  7258  nninfninc  7286  nnnninfeq  7291  nnnninfeq2  7292  nninfwlpoimlemg  7338  nninfwlpoimlemginf  7339  nninfwlpoim  7342  nninfinfwlpo  7343  indpi  7525  ennnfoneleminc  12977  ennnfonelemex  12980  bj-indsuc  16249  bj-bdfindes  16270  bj-nn0suc0  16271  bj-peano4  16276  bj-inf2vnlem1  16291  bj-nn0sucALT  16299  bj-findes  16302  nnsf  16330  nninfsellemdc  16335  nninfself  16338  nninfsellemeqinf  16341  nninfomni  16344