HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  chshii Unicode version

Theorem chshii 22683
Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
Hypothesis
Ref Expression
chshi.1  |-  H  e. 
CH
Assertion
Ref Expression
chshii  |-  H  e.  SH

Proof of Theorem chshii
StepHypRef Expression
1 chshi.1 . 2  |-  H  e. 
CH
2 chsh 22680 . 2  |-  ( H  e.  CH  ->  H  e.  SH )
31, 2ax-mp 8 1  |-  H  e.  SH
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   SHcsh 22384   CHcch 22385
This theorem is referenced by:  chssii  22687  helsh  22700  h0elsh  22711  hhsscms  22732  hhssbn  22733  hhsshl  22734  chocunii  22756  shsleji  22825  shjshcli  22831  pjhthlem1  22846  pjhthlem2  22847  omlsii  22858  ococi  22860  pjoc1i  22886  chne0i  22908  chocini  22909  chjcli  22912  chsleji  22913  chseli  22914  chunssji  22922  chjcomi  22923  chub1i  22924  chlubi  22926  chlej1i  22928  chlej2i  22929  h1de2bi  23009  h1de2ctlem  23010  spansnpji  23033  spanunsni  23034  h1datomi  23036  pjoml2i  23040  qlaxr3i  23091  osumi  23097  osumcor2i  23099  spansnji  23101  spansnm0i  23105  nonbooli  23106  spansncvi  23107  5oai  23116  3oalem2  23118  3oalem5  23121  3oalem6  23122  pjaddii  23130  pjmulii  23132  pjss2i  23135  pjssmii  23136  pj0i  23148  pjocini  23153  pjjsi  23155  pjpythi  23177  mayete3i  23183  mayete3iOLD  23184  pjnmopi  23604  pjimai  23632  pjclem4  23655  pj3si  23663  sto1i  23692  stlei  23696  strlem1  23706  hatomici  23815  hatomistici  23818  atomli  23838  chirredlem3  23848  sumdmdii  23871  sumdmdlem  23874  sumdmdlem2  23875
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-xp 4843  df-cnv 4845  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fv 5421  df-ov 6043  df-ch 22677
  Copyright terms: Public domain W3C validator