Theorem sheli 30325

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

Syntax hints:   → wi 4   ∈ wcel 2106   ℋchba 30030   S_ℋ csh 30039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5289  ax-hilex 30110

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3430  df-v 3472  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4520  df-pw 4595  df-sn 4620  df-pr 4622  df-op 4626  df-br 5139  df-opab 5201  df-xp 5672  df-cnv 5674  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-sh 30318

This theorem is referenced by:  norm1exi  30361  hhssabloi  30373  hhssnv  30375  shscli  30428  shunssi  30479  shmodsi  30500  omlsii  30514  5oalem1  30765  5oalem2  30766  5oalem3  30767  5oalem5  30769  imaelshi  31169  pjimai  31287  shatomici  31469  shatomistici  31472  cdjreui  31543  cdj1i  31544  cdj3lem1  31545  cdj3lem2b  31548  cdj3lem3  31549  cdj3lem3b  31551  cdj3i  31552