Theorem sheli 31577

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142   ℋchba 31282   S_ℋ csh 31291

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-hilex 31362

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-xp 5666  df-cnv 5668  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-sh 31570

This theorem is used by:  norm1exi  31613  hhssabloi  31625  hhssnv  31627  shscli  31680  shunssi  31731  shmodsi  31752  omlsii  31766  5oalem1  32017  5oalem2  32018  5oalem3  32019  5oalem5  32021  imaelshi  32421  pjimai  32539  shatomici  32721  shatomistici  32724  cdjreui  32795  cdj1i  32796  cdj3lem1  32797  cdj3lem2b  32800  cdj3lem3  32801  cdj3lem3b  32803  cdj3i  32804