Theorem suceq 4157

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 3409	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3127	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4126	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4126	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2138	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1284   ∪ cun 2971  {csn 3398  suc csuc 4120

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-sn 3404  df-suc 4126

This theorem is referenced by:  eqelsuc  4174  2ordpr  4267  onsucsssucexmid  4270  onsucelsucexmid  4273  ordsucunielexmid  4274  suc11g  4300  onsucuni2  4307  0elsucexmid  4308  ordpwsucexmid  4313  peano2  4336  findes  4344  nn0suc  4345  0elnn  4358  frecsuc  6014  sucinc  6048  sucinc2  6049  oacl  6063  oav2  6066  oasuc  6067  oa1suc  6070  nna0r  6080  nnacom  6086  nnaass  6087  nnmsucr  6090  nnsucelsuc  6093  nnsucsssuc  6094  nnaword  6107  nnaordex  6123  phplem3g  6342  nneneq  6343  php5  6344  php5dom  6349  indpi  6532  bj-indsuc  10723  bj-bdfindes  10744  bj-nn0suc0  10745  bj-peano4  10750  bj-inf2vnlem1  10765  bj-nn0sucALT  10773  bj-findes  10776