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

Theorem chshii 21862
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 21859 . 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 1701   SHcsh 21563   CHcch 21564
This theorem is referenced by:  chssii  21866  helsh  21879  h0elsh  21890  hhsscms  21911  hhssbn  21912  hhsshl  21913  chocunii  21935  shsleji  22004  shjshcli  22010  pjhthlem1  22025  pjhthlem2  22026  omlsii  22037  ococi  22039  pjoc1i  22065  chne0i  22087  chocini  22088  chjcli  22091  chsleji  22092  chseli  22093  chunssji  22101  chjcomi  22102  chub1i  22103  chlubi  22105  chlej1i  22107  chlej2i  22108  h1de2bi  22188  h1de2ctlem  22189  spansnpji  22212  spanunsni  22213  h1datomi  22215  pjoml2i  22219  qlaxr3i  22270  osumi  22276  osumcor2i  22278  spansnji  22280  spansnm0i  22284  nonbooli  22285  spansncvi  22286  5oai  22295  3oalem2  22297  3oalem5  22300  3oalem6  22301  pjaddii  22309  pjmulii  22311  pjss2i  22314  pjssmii  22315  pj0i  22327  pjocini  22332  pjjsi  22334  pjpythi  22356  mayete3i  22362  mayete3iOLD  22363  pjnmopi  22783  pjimai  22811  pjclem4  22834  pj3si  22842  sto1i  22871  stlei  22875  strlem1  22885  hatomici  22994  hatomistici  22997  atomli  23017  chirredlem3  23027  sumdmdii  23050  sumdmdlem  23053  sumdmdlem2  23054
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-xp 4732  df-cnv 4734  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fv 5300  df-ov 5903  df-ch 21856
  Copyright terms: Public domain W3C validator