Theorem suceq 4497

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

Syntax hints:   → wi 4   = wceq 1395   ∪ cun 3196  {csn 3667  suc csuc 4460

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 2802  df-un 3202  df-sn 3673  df-suc 4466

This theorem is referenced by:  eqelsuc  4514  2ordpr  4620  onsucsssucexmid  4623  onsucelsucexmid  4626  ordsucunielexmid  4627  suc11g  4653  onsucuni2  4660  0elsucexmid  4661  ordpwsucexmid  4666  peano2  4691  findes  4699  nn0suc  4700  0elnn  4715  omsinds  4718  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  tfrcl  6525  frecabcl  6560  frecsuc  6568  sucinc  6608  sucinc2  6609  oacl  6623  oav2  6626  oasuc  6627  oa1suc  6630  nna0r  6641  nnacom  6647  nnaass  6648  nnmsucr  6651  nnsucelsuc  6654  nnsucsssuc  6655  nnaword  6674  nnaordex  6691  phplem3g  7037  nneneq  7038  php5  7039  php5dom  7044  omp1eomlem  7284  omp1eom  7285  nninfninc  7313  nnnninfeq  7318  nnnninfeq2  7319  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  nninfwlpoim  7369  nninfinfwlpo  7370  indpi  7552  ennnfoneleminc  13022  ennnfonelemex  13025  bj-indsuc  16459  bj-bdfindes  16480  bj-nn0suc0  16481  bj-peano4  16486  bj-inf2vnlem1  16501  bj-nn0sucALT  16509  bj-findes  16512  nnsf  16543  nninfsellemdc  16548  nninfself  16551  nninfsellemeqinf  16554  nninfomni  16557