Theorem suceq 4403

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 3604	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3291	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4372	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4372	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2235	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1353   ∪ cun 3128  {csn 3593  suc csuc 4366

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-suc 4372

This theorem is referenced by:  eqelsuc  4420  2ordpr  4524  onsucsssucexmid  4527  onsucelsucexmid  4530  ordsucunielexmid  4531  suc11g  4557  onsucuni2  4564  0elsucexmid  4565  ordpwsucexmid  4570  peano2  4595  findes  4603  nn0suc  4604  0elnn  4619  omsinds  4622  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  tfrcl  6365  frecabcl  6400  frecsuc  6408  sucinc  6446  sucinc2  6447  oacl  6461  oav2  6464  oasuc  6465  oa1suc  6468  nna0r  6479  nnacom  6485  nnaass  6486  nnmsucr  6489  nnsucelsuc  6492  nnsucsssuc  6493  nnaword  6512  nnaordex  6529  phplem3g  6856  nneneq  6857  php5  6858  php5dom  6863  omp1eomlem  7093  omp1eom  7094  nnnninfeq  7126  nnnninfeq2  7127  nninfwlpoimlemg  7173  nninfwlpoimlemginf  7174  nninfwlpoim  7176  indpi  7341  ennnfoneleminc  12412  ennnfonelemex  12415  bj-indsuc  14683  bj-bdfindes  14704  bj-nn0suc0  14705  bj-peano4  14710  bj-inf2vnlem1  14725  bj-nn0sucALT  14733  bj-findes  14736  nnsf  14757  nninfsellemdc  14762  nninfself  14765  nninfsellemeqinf  14768  nninfomni  14771