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

Theorem chssii 21866
Description: A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)
Hypothesis
Ref Expression
chssi.1  |-  H  e. 
CH
Assertion
Ref Expression
chssii  |-  H  C_  ~H

Proof of Theorem chssii
StepHypRef Expression
1 chssi.1 . . 3  |-  H  e. 
CH
21chshii 21862 . 2  |-  H  e.  SH
32shssii 21847 1  |-  H  C_  ~H
Colors of variables: wff set class
Syntax hints:    e. wcel 1701    C_ wss 3186   ~Hchil 21554   CHcch 21564
This theorem is referenced by:  cheli  21867  chelii  21868  hhsscms  21911  chocvali  21933  chm1i  22090  chsscon3i  22095  chsscon2i  22097  chjoi  22122  chj1i  22123  shjshsi  22126  sshhococi  22180  h1dei  22184  spansnpji  22212  spanunsni  22213  h1datomi  22215  spansnji  22280  pjfi  22338  riesz3i  22697  hmopidmpji  22787  pjoccoi  22813  pjinvari  22826  stcltr2i  22910  mdsymi  23046  mdcompli  23064  dmdcompli  23065
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  ax-sep 4178  ax-hilex 21634
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-pw 3661  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-sh 21841  df-ch 21856
  Copyright terms: Public domain W3C validator