Theorem chssii 31327

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

Syntax hints:   ∈ wcel 2119   ⊆ wss 3890   ℋchba 31015   C_ℋ cch 31025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-hilex 31095

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fv 6500  df-ov 7366  df-sh 31303  df-ch 31317

This theorem is referenced by:  cheli  31328  chelii  31329  hhsscms  31374  chocvali  31395  chm1i  31552  chsscon3i  31557  chsscon2i  31559  chjoi  31584  chj1i  31585  shjshsi  31588  sshhococi  31642  h1dei  31646  spansnpji  31674  spanunsni  31675  h1datomi  31677  spansnji  31742  pjfi  31800  riesz3i  32158  hmopidmpji  32248  pjoccoi  32274  pjinvari  32287  stcltr2i  32371  mdsymi  32507  mdcompli  32525  dmdcompli  32526