Theorem suceq 4542

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 3716	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3384	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4511	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4511	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2296	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1402   ∪ cun 3218  {csn 3705  suc csuc 4505

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-suc 4511

This theorem is referenced by:  eqelsuc  4559  2ordpr  4666  onsucsssucexmid  4669  onsucelsucexmid  4672  ordsucunielexmid  4673  suc11g  4699  onsucuni2  4706  0elsucexmid  4707  ordpwsucexmid  4712  peano2  4737  findes  4745  nn0suc  4746  0elnn  4761  omsinds  4764  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  tfrcl  6625  frecabcl  6660  frecsuc  6668  sucinc  6708  sucinc2  6709  oacl  6723  oav2  6726  oasuc  6727  oa1suc  6730  nna0r  6741  nnacom  6747  nnaass  6748  nnmsucr  6751  nnsucelsuc  6754  nnsucsssuc  6755  nnaword  6774  nnaordex  6791  phplem3g  7147  nneneq  7148  php5  7149  php5dom  7154  omp1eomlem  7424  omp1eom  7425  nninfninc  7453  nnnninfeq  7458  nnnninfeq2  7459  nninfwlpoimlemg  7505  nninfwlpoimlemginf  7506  nninfwlpoim  7509  nninfinfwlpo  7510  indpi  7699  ennnfoneleminc  13280  ennnfonelemex  13283  bj-indsuc  16868  bj-bdfindes  16889  bj-nn0suc0  16890  bj-peano4  16895  bj-inf2vnlem1  16910  bj-nn0sucALT  16918  bj-findes  16921  nnsf  16953  nninfsellemdc  16958  nninfself  16961  nninfsellemeqinf  16964  nninfomni  16967