Theorem sheli 31352

Description: A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)

Hypothesis

Ref	Expression
shssi.1	⊢ 𝐻 ∈ Sℋ

Assertion

Ref	Expression
sheli	⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Proof of Theorem sheli

Step	Hyp	Ref	Expression
1		shssi.1	. . 3 ⊢ 𝐻 ∈ Sℋ
2	1	shssii 31351	. 2 ⊢ 𝐻 ⊆ ℋ
3	2	sseli 3923	1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Syntax hints:   → wi 4   ∈ wcel 2132   ℋchba 31057   S_ℋ csh 31066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-hilex 31137

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-opab 5153  df-xp 5642  df-cnv 5644  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-sh 31345

This theorem is referenced by:  norm1exi  31388  hhssabloi  31400  hhssnv  31402  shscli  31455  shunssi  31506  shmodsi  31527  omlsii  31541  5oalem1  31792  5oalem2  31793  5oalem3  31794  5oalem5  31796  imaelshi  32196  pjimai  32314  shatomici  32496  shatomistici  32499  cdjreui  32570  cdj1i  32571  cdj3lem1  32572  cdj3lem2b  32575  cdj3lem3  32576  cdj3lem3b  32578  cdj3i  32579