Theorem suceq 4434

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 3630	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3315	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 4403	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 4403	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2251	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1364   ∪ cun 3152  {csn 3619  suc csuc 4397

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-suc 4403

This theorem is referenced by:  eqelsuc  4451  2ordpr  4557  onsucsssucexmid  4560  onsucelsucexmid  4563  ordsucunielexmid  4564  suc11g  4590  onsucuni2  4597  0elsucexmid  4598  ordpwsucexmid  4603  peano2  4628  findes  4636  nn0suc  4637  0elnn  4652  omsinds  4655  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  tfrcl  6419  frecabcl  6454  frecsuc  6462  sucinc  6500  sucinc2  6501  oacl  6515  oav2  6518  oasuc  6519  oa1suc  6522  nna0r  6533  nnacom  6539  nnaass  6540  nnmsucr  6543  nnsucelsuc  6546  nnsucsssuc  6547  nnaword  6566  nnaordex  6583  phplem3g  6914  nneneq  6915  php5  6916  php5dom  6921  omp1eomlem  7155  omp1eom  7156  nninfninc  7184  nnnninfeq  7189  nnnninfeq2  7190  nninfwlpoimlemg  7236  nninfwlpoimlemginf  7237  nninfwlpoim  7239  indpi  7404  ennnfoneleminc  12571  ennnfonelemex  12574  bj-indsuc  15490  bj-bdfindes  15511  bj-nn0suc0  15512  bj-peano4  15517  bj-inf2vnlem1  15532  bj-nn0sucALT  15540  bj-findes  15543  nnsf  15565  nninfsellemdc  15570  nninfself  15573  nninfsellemeqinf  15576  nninfomni  15579