Theorem chssii 28397

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	⊢ 𝐻 ∈ Cℋ

Assertion

Ref	Expression
chssii	⊢ 𝐻 ⊆ ℋ

Proof of Theorem chssii

Step	Hyp	Ref	Expression
1		chssi.1	. . 3 ⊢ 𝐻 ∈ Cℋ
2	1	chshii 28393	. 2 ⊢ 𝐻 ∈ Sℋ
3	2	shssii 28379	1 ⊢ 𝐻 ⊆ ℋ

Syntax hints:   ∈ wcel 2139   ⊆ wss 3715   ℋchil 28085   C_ℋ cch 28095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-hilex 28165

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-xp 5272  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fv 6057  df-ov 6816  df-sh 28373  df-ch 28387

This theorem is referenced by:  cheli  28398  chelii  28399  hhsscms  28445  chocvali  28467  chm1i  28624  chsscon3i  28629  chsscon2i  28631  chjoi  28656  chj1i  28657  shjshsi  28660  sshhococi  28714  h1dei  28718  spansnpji  28746  spanunsni  28747  h1datomi  28749  spansnji  28814  pjfi  28872  riesz3i  29230  hmopidmpji  29320  pjoccoi  29346  pjinvari  29359  stcltr2i  29443  mdsymi  29579  mdcompli  29597  dmdcompli  29598