Theorem suceq 4449

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 3644	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3328	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4418	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4418	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2263	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1373   ∪ cun 3164  {csn 3633  suc csuc 4412

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-suc 4418

This theorem is referenced by:  eqelsuc  4466  2ordpr  4572  onsucsssucexmid  4575  onsucelsucexmid  4578  ordsucunielexmid  4579  suc11g  4605  onsucuni2  4612  0elsucexmid  4613  ordpwsucexmid  4618  peano2  4643  findes  4651  nn0suc  4652  0elnn  4667  omsinds  4670  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  tfrcl  6450  frecabcl  6485  frecsuc  6493  sucinc  6531  sucinc2  6532  oacl  6546  oav2  6549  oasuc  6550  oa1suc  6553  nna0r  6564  nnacom  6570  nnaass  6571  nnmsucr  6574  nnsucelsuc  6577  nnsucsssuc  6578  nnaword  6597  nnaordex  6614  phplem3g  6953  nneneq  6954  php5  6955  php5dom  6960  omp1eomlem  7196  omp1eom  7197  nninfninc  7225  nnnninfeq  7230  nnnninfeq2  7231  nninfwlpoimlemg  7277  nninfwlpoimlemginf  7278  nninfwlpoim  7281  nninfinfwlpo  7282  indpi  7455  ennnfoneleminc  12782  ennnfonelemex  12785  bj-indsuc  15864  bj-bdfindes  15885  bj-nn0suc0  15886  bj-peano4  15891  bj-inf2vnlem1  15906  bj-nn0sucALT  15914  bj-findes  15917  nnsf  15942  nninfsellemdc  15947  nninfself  15950  nninfsellemeqinf  15953  nninfomni  15956