Theorem suceq 4401

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

Syntax hints:   → wi 4   = wceq 1353   ∪ cun 3127  {csn 3592  suc csuc 4364

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 2739  df-un 3133  df-sn 3598  df-suc 4370

This theorem is referenced by:  eqelsuc  4418  2ordpr  4522  onsucsssucexmid  4525  onsucelsucexmid  4528  ordsucunielexmid  4529  suc11g  4555  onsucuni2  4562  0elsucexmid  4563  ordpwsucexmid  4568  peano2  4593  findes  4601  nn0suc  4602  0elnn  4617  omsinds  4620  tfr1onlemsucaccv  6339  tfrcllemsucaccv  6352  tfrcl  6362  frecabcl  6397  frecsuc  6405  sucinc  6443  sucinc2  6444  oacl  6458  oav2  6461  oasuc  6462  oa1suc  6465  nna0r  6476  nnacom  6482  nnaass  6483  nnmsucr  6486  nnsucelsuc  6489  nnsucsssuc  6490  nnaword  6509  nnaordex  6526  phplem3g  6853  nneneq  6854  php5  6855  php5dom  6860  omp1eomlem  7090  omp1eom  7091  nnnninfeq  7123  nnnninfeq2  7124  nninfwlpoimlemg  7170  nninfwlpoimlemginf  7171  nninfwlpoim  7173  indpi  7338  ennnfoneleminc  12404  ennnfonelemex  12407  bj-indsuc  14540  bj-bdfindes  14561  bj-nn0suc0  14562  bj-peano4  14567  bj-inf2vnlem1  14582  bj-nn0sucALT  14590  bj-findes  14593  nnsf  14614  nninfsellemdc  14619  nninfself  14622  nninfsellemeqinf  14625  nninfomni  14628