Theorem chssii 29494

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 29490	. 2 ⊢ 𝐻 ∈ Sℋ
3	2	shssii 29476	1 ⊢ 𝐻 ⊆ ℋ

Syntax hints:   ∈ wcel 2108   ⊆ wss 3883   ℋchba 29182   C_ℋ cch 29192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-hilex 29262

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fv 6426  df-ov 7258  df-sh 29470  df-ch 29484

This theorem is referenced by:  cheli  29495  chelii  29496  hhsscms  29541  chocvali  29562  chm1i  29719  chsscon3i  29724  chsscon2i  29726  chjoi  29751  chj1i  29752  shjshsi  29755  sshhococi  29809  h1dei  29813  spansnpji  29841  spanunsni  29842  h1datomi  29844  spansnji  29909  pjfi  29967  riesz3i  30325  hmopidmpji  30415  pjoccoi  30441  pjinvari  30454  stcltr2i  30538  mdsymi  30674  mdcompli  30692  dmdcompli  30693