Theorem chssii 29266

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

Syntax hints:   ∈ wcel 2112   ⊆ wss 3853   ℋchba 28954   C_ℋ cch 28964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-hilex 29034

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-xp 5542  df-cnv 5544  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fv 6366  df-ov 7194  df-sh 29242  df-ch 29256

This theorem is referenced by:  cheli  29267  chelii  29268  hhsscms  29313  chocvali  29334  chm1i  29491  chsscon3i  29496  chsscon2i  29498  chjoi  29523  chj1i  29524  shjshsi  29527  sshhococi  29581  h1dei  29585  spansnpji  29613  spanunsni  29614  h1datomi  29616  spansnji  29681  pjfi  29739  riesz3i  30097  hmopidmpji  30187  pjoccoi  30213  pjinvari  30226  stcltr2i  30310  mdsymi  30446  mdcompli  30464  dmdcompli  30465