Theorem sheli 31750

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ℋchba 31455   S_ℋ csh 31464

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5248  ax-hilex 31535

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  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 5653  df-cnv 5655  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-sh 31743

This theorem is used by:  norm1exi  31786  hhssabloi  31798  hhssnv  31800  shscli  31853  shunssi  31904  shmodsi  31925  omlsii  31939  5oalem1  32190  5oalem2  32191  5oalem3  32192  5oalem5  32194  imaelshi  32594  pjimai  32712  shatomici  32894  shatomistici  32897  cdjreui  32968  cdj1i  32969  cdj3lem1  32970  cdj3lem2b  32973  cdj3lem3  32974  cdj3lem3b  32976  cdj3i  32977