ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  suceq GIF version

Theorem suceq 4220
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
StepHypRef Expression
1 id 19 . . 3 (𝐴 = 𝐵𝐴 = 𝐵)
2 sneq 3452 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
31, 2uneq12d 3153 . 2 (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4 df-suc 4189 . 2 suc 𝐴 = (𝐴 ∪ {𝐴})
5 df-suc 4189 . 2 suc 𝐵 = (𝐵 ∪ {𝐵})
63, 4, 53eqtr4g 2145 1 (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  cun 2995  {csn 3441  suc csuc 4183
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-sn 3447  df-suc 4189
This theorem is referenced by:  eqelsuc  4237  2ordpr  4330  onsucsssucexmid  4333  onsucelsucexmid  4336  ordsucunielexmid  4337  suc11g  4363  onsucuni2  4370  0elsucexmid  4371  ordpwsucexmid  4376  peano2  4400  findes  4408  nn0suc  4409  0elnn  4422  omsinds  4425  tfr1onlemsucaccv  6088  tfrcllemsucaccv  6101  tfrcl  6111  frecabcl  6146  frecsuc  6154  sucinc  6188  sucinc2  6189  oacl  6203  oav2  6206  oasuc  6207  oa1suc  6210  nna0r  6221  nnacom  6227  nnaass  6228  nnmsucr  6231  nnsucelsuc  6234  nnsucsssuc  6235  nnaword  6250  nnaordex  6266  phplem3g  6552  nneneq  6553  php5  6554  php5dom  6559  indpi  6880  bj-indsuc  11469  bj-bdfindes  11490  bj-nn0suc0  11491  bj-peano4  11496  bj-inf2vnlem1  11511  bj-nn0sucALT  11519  bj-findes  11522  nnsf  11541  nninfalllemn  11544  nninfsellemdc  11548  nninfself  11551  nninfsellemeqinf  11554  nninfomni  11557
  Copyright terms: Public domain W3C validator