Metamath Proof Explorer

Theorem sheli

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

Ref Expression
Hypothesis shssi.1 H S
Assertion sheli A H A


Step Hyp Ref Expression
1 shssi.1 H S
2 1 shssii H
3 2 sseli A H A