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

Theorem chshii 26559
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 26556 . 2  |-  ( H  e.  CH  ->  H  e.  SH )
31, 2ax-mp 5 1  |-  H  e.  SH
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842   SHcsh 26259   CHcch 26260
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-xp 4829  df-cnv 4831  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fv 5577  df-ov 6281  df-ch 26553
This theorem is referenced by:  chssii  26563  helsh  26577  h0elsh  26588  hhsscms  26609  hhssbn  26610  hhsshl  26611  chocunii  26633  shsleji  26702  shjshcli  26708  pjhthlem1  26723  pjhthlem2  26724  omlsii  26735  ococi  26737  pjoc1i  26763  chne0i  26785  chocini  26786  chjcli  26789  chsleji  26790  chseli  26791  chunssji  26799  chjcomi  26800  chub1i  26801  chlubi  26803  chlej1i  26805  chlej2i  26806  h1de2bi  26886  h1de2ctlem  26887  spansnpji  26910  spanunsni  26911  h1datomi  26913  pjoml2i  26917  qlaxr3i  26968  osumi  26974  osumcor2i  26976  spansnji  26978  spansnm0i  26982  nonbooli  26983  spansncvi  26984  5oai  26993  3oalem2  26995  3oalem5  26998  3oalem6  26999  pjaddii  27007  pjmulii  27009  pjss2i  27012  pjssmii  27013  pj0i  27025  pjocini  27030  pjjsi  27032  pjpythi  27054  mayete3i  27060  pjnmopi  27480  pjimai  27508  pjclem4  27531  pj3si  27539  sto1i  27568  stlei  27572  strlem1  27582  hatomici  27691  hatomistici  27694  atomli  27714  chirredlem3  27724  sumdmdii  27747  sumdmdlem  27750  sumdmdlem2  27751
  Copyright terms: Public domain W3C validator