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

Theorem suceq 4196
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 3436 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2uneq12d 3141 . 2  |-  ( A  =  B  ->  ( A  u.  { A } )  =  ( B  u.  { B } ) )
4 df-suc 4165 . 2  |-  suc  A  =  ( A  u.  { A } )
5 df-suc 4165 . 2  |-  suc  B  =  ( B  u.  { B } )
63, 4, 53eqtr4g 2142 1  |-  ( A  =  B  ->  suc  A  =  suc  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1287    u. cun 2984   {csn 3425   suc csuc 4159
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 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2616  df-un 2990  df-sn 3431  df-suc 4165
This theorem is referenced by:  eqelsuc  4213  2ordpr  4306  onsucsssucexmid  4309  onsucelsucexmid  4312  ordsucunielexmid  4313  suc11g  4339  onsucuni2  4346  0elsucexmid  4347  ordpwsucexmid  4352  peano2  4376  findes  4384  nn0suc  4385  0elnn  4398  omsinds  4401  tfr1onlemsucaccv  6041  tfrcllemsucaccv  6054  tfrcl  6064  frecabcl  6099  frecsuc  6107  sucinc  6141  sucinc2  6142  oacl  6156  oav2  6159  oasuc  6160  oa1suc  6163  nna0r  6174  nnacom  6180  nnaass  6181  nnmsucr  6184  nnsucelsuc  6187  nnsucsssuc  6188  nnaword  6203  nnaordex  6219  phplem3g  6505  nneneq  6506  php5  6507  php5dom  6512  indpi  6822  bj-indsuc  11180  bj-bdfindes  11201  bj-nn0suc0  11202  bj-peano4  11207  bj-inf2vnlem1  11222  bj-nn0sucALT  11230  bj-findes  11233  nnsf  11251  nninfalllemn  11254  nninfsellemdc  11258  nninfself  11261  nninfsellemeqinf  11264  nninfomni  11267
  Copyright terms: Public domain W3C validator