Theorem suceq 4387

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 3594	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3282	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4356	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4356	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2228	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1348   ∪ cun 3119  {csn 3583  suc csuc 4350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-suc 4356

This theorem is referenced by:  eqelsuc  4404  2ordpr  4508  onsucsssucexmid  4511  onsucelsucexmid  4514  ordsucunielexmid  4515  suc11g  4541  onsucuni2  4548  0elsucexmid  4549  ordpwsucexmid  4554  peano2  4579  findes  4587  nn0suc  4588  0elnn  4603  omsinds  4606  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  tfrcl  6343  frecabcl  6378  frecsuc  6386  sucinc  6424  sucinc2  6425  oacl  6439  oav2  6442  oasuc  6443  oa1suc  6446  nna0r  6457  nnacom  6463  nnaass  6464  nnmsucr  6467  nnsucelsuc  6470  nnsucsssuc  6471  nnaword  6490  nnaordex  6507  phplem3g  6834  nneneq  6835  php5  6836  php5dom  6841  omp1eomlem  7071  omp1eom  7072  nnnninfeq  7104  nnnninfeq2  7105  nninfwlpoimlemg  7151  nninfwlpoimlemginf  7152  nninfwlpoim  7154  indpi  7304  ennnfoneleminc  12366  ennnfonelemex  12369  bj-indsuc  13963  bj-bdfindes  13984  bj-nn0suc0  13985  bj-peano4  13990  bj-inf2vnlem1  14005  bj-nn0sucALT  14013  bj-findes  14016  nnsf  14038  nninfsellemdc  14043  nninfself  14046  nninfsellemeqinf  14049  nninfomni  14052