Theorem sheli 31817

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 31816	. 2 ⊢ 𝐻 ⊆ ℋ
3	2	sseli 3904	1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ℋchba 31522   S_ℋ csh 31531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-hilex 31602

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-sh 31810

This theorem is used by:  norm1exi  31853  hhssabloi  31865  hhssnv  31867  shscli  31920  shunssi  31971  shmodsi  31992  omlsii  32006  5oalem1  32257  5oalem2  32258  5oalem3  32259  5oalem5  32261  imaelshi  32661  pjimai  32779  shatomici  32961  shatomistici  32964  cdjreui  33035  cdj1i  33036  cdj3lem1  33037  cdj3lem2b  33040  cdj3lem3  33041  cdj3lem3b  33043  cdj3i  33044