Theorem shssii 31636

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 31633	. 2 ⊢ (𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ)
3	1, 2	ax-mp 5	1 ⊢ 𝐻 ⊆ ℋ

This proof depends on syntax axioms:   ∈ wcel 2146   ⊆ wss 3906   ℋchba 31342   S_ℋ csh 31351

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-hilex 31422

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-sh 31630

This theorem is used by:  sheli  31637  shelii  31638  chssii  31654  hhssabloilem  31684  hhssabloi  31685  hhssnv  31687  hhssba  31694  shunssji  31792  shsval3i  31811  shjshsi  31915  span0  31965  spanuni  31967  imaelshi  32481  nlelchi  32484  hmopidmchi  32574  pjimai  32599  shatomistici  32784