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

Theorem suceq 4105
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 3378 . . 3 (A = B → {A} = {B})
31, 2uneq12d 3092 . 2 (A = B → (A ∪ {A}) = (B ∪ {B}))
4 df-suc 4074 . 2 suc A = (A ∪ {A})
5 df-suc 4074 . 2 suc B = (B ∪ {B})
63, 4, 53eqtr4g 2094 1 (A = B → suc A = suc B)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242  cun 2909  {csn 3367  suc csuc 4068
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-sn 3373  df-suc 4074
This theorem is referenced by:  eqelsuc  4122  onsucsssucexmid  4212  onsucelsucexmidlem  4214  onsucelsucexmid  4215  ordsucunielexmid  4216  suc11g  4235  ordpwsucexmid  4246  peano2  4261  findes  4269  nn0suc  4270  0elnn  4283  frecsuc  5930  sucinc  5964  sucinc2  5965  oacl  5979  oav2  5982  oasuc  5983  oa1suc  5986  nna0r  5996  nnacom  6002  nnaass  6003  nnmsucr  6006  nnsucelsuc  6009  nnsucsssuc  6010  nnaword  6020  nnaordex  6036  indpi  6326  bj-indsuc  9363  bj-bdfindes  9383  bj-nn0suc0  9384  bj-peano4  9389  bj-inf2vnlem1  9400  bj-nn0sucALT  9408  bj-findes  9411
  Copyright terms: Public domain W3C validator