Theorem shssii 29562

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
shssi.1	⊢ 𝐻 ∈ Sℋ

Assertion

Ref	Expression
shssii	⊢ 𝐻 ⊆ ℋ

Proof of Theorem shssii

Step	Hyp	Ref	Expression
1		shssi.1	. 2 ⊢ 𝐻 ∈ Sℋ
2		shss 29559	. 2 ⊢ (𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ)
3	1, 2	ax-mp 5	1 ⊢ 𝐻 ⊆ ℋ

Syntax hints:   ∈ wcel 2106   ⊆ wss 3888   ℋchba 29268   S_ℋ csh 29277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-hilex 29348

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-br 5076  df-opab 5138  df-xp 5592  df-cnv 5594  df-dm 5596  df-rn 5597  df-res 5598  df-ima 5599  df-sh 29556

This theorem is referenced by:  sheli  29563  shelii  29564  chssii  29580  hhssabloilem  29610  hhssabloi  29611  hhssnv  29613  hhssba  29620  shunssji  29718  shsval3i  29737  shjshsi  29841  span0  29891  spanuni  29893  imaelshi  30407  nlelchi  30410  hmopidmchi  30500  pjimai  30525  shatomistici  30710