Theorem suceq 4238

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 3461	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3156	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4207	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4207	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2146	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1290   ∪ cun 2998  {csn 3450  suc csuc 4201

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2622  df-un 3004  df-sn 3456  df-suc 4207

This theorem is referenced by:  eqelsuc  4255  2ordpr  4353  onsucsssucexmid  4356  onsucelsucexmid  4359  ordsucunielexmid  4360  suc11g  4386  onsucuni2  4393  0elsucexmid  4394  ordpwsucexmid  4399  peano2  4423  findes  4431  nn0suc  4432  0elnn  4445  omsinds  4448  tfr1onlemsucaccv  6120  tfrcllemsucaccv  6133  tfrcl  6143  frecabcl  6178  frecsuc  6186  sucinc  6220  sucinc2  6221  oacl  6235  oav2  6238  oasuc  6239  oa1suc  6242  nna0r  6253  nnacom  6259  nnaass  6260  nnmsucr  6263  nnsucelsuc  6266  nnsucsssuc  6267  nnaword  6284  nnaordex  6300  phplem3g  6626  nneneq  6627  php5  6628  php5dom  6633  indpi  6962  bj-indsuc  12096  bj-bdfindes  12117  bj-nn0suc0  12118  bj-peano4  12123  bj-inf2vnlem1  12138  bj-nn0sucALT  12146  bj-findes  12149  nnsf  12167  nninfalllemn  12170  nninfsellemdc  12174  nninfself  12177  nninfsellemeqinf  12180  nninfomni  12183