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

Theorem suceq 4084
Description: Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
suceq (A = B → suc A = suc B)

Proof of Theorem suceq
StepHypRef Expression
1 id 19 . . 3 (A = BA = B)
2 sneq 3357 . . 3 (A = B → {A} = {B})
31, 2uneq12d 3071 . 2 (A = B → (A ∪ {A}) = (B ∪ {B}))
4 df-suc 4053 . 2 suc A = (A ∪ {A})
5 df-suc 4053 . 2 suc B = (B ∪ {B})
63, 4, 53eqtr4g 2075 1 (A = B → suc A = suc B)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1226  cun 2888  {csn 3346  suc csuc 4047
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-un 2895  df-sn 3352  df-suc 4053
This theorem is referenced by:  eqelsuc  4101  onsucsssucexmid  4192  onsucelsucexmidlem  4194  onsucelsucexmid  4195  ordsucunielexmid  4196  suc11g  4215  ordpwsucexmid  4226  peano2  4241  findes  4249  nn0suc  4250  0elnn  4263  frecsuc  5903  sucinc  5936  sucinc2  5937  oacl  5951  oav2  5954  oasuc  5955  oa1suc  5958  nna0r  5968  nnacom  5974  nnaass  5975  nnmsucr  5978  nnsucelsuc  5981  nnsucsssuc  5982  nnaword  5991  nnaordex  6007  bj-indsuc  7290  bj-bdfindes  7310  bj-nn0suc0  7311  bj-peano4  7316  bj-inf2vnlem1  7327  bj-nn0sucALT  7335  bj-findes  7338
  Copyright terms: Public domain W3C validator