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

Theorem suceq 4166
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  =  B  ->  A  =  B )
2 sneq 3413 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3125 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4135 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4135 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2113 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259    u. cun 2942   {csn 3402   suc csuc 4129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-un 2949  df-sn 3408  df-suc 4135
This theorem is referenced by:  eqelsuc  4183  2ordpr  4276  onsucsssucexmid  4279  onsucelsucexmid  4282  ordsucunielexmid  4283  suc11g  4308  onsucuni2  4315  0elsucexmid  4316  ordpwsucexmid  4321  peano2  4345  findes  4353  nn0suc  4354  0elnn  4367  frecsuc  6021  sucinc  6055  sucinc2  6056  oacl  6070  oav2  6073  oasuc  6074  oa1suc  6077  nna0r  6087  nnacom  6093  nnaass  6094  nnmsucr  6097  nnsucelsuc  6100  nnsucsssuc  6101  nnaword  6114  nnaordex  6130  phplem3g  6349  nneneq  6350  php5  6351  php5dom  6355  indpi  6497  bj-indsuc  10411  bj-bdfindes  10433  bj-nn0suc0  10434  bj-peano4  10439  bj-inf2vnlem1  10454  bj-nn0sucALT  10462  bj-findes  10465
  Copyright terms: Public domain W3C validator