Description: A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 14-Dec-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | shel | |- ( ( H e. SH /\ A e. H ) -> A e. ~H ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shss | |- ( H e. SH -> H C_ ~H ) |
|
2 | 1 | sselda | |- ( ( H e. SH /\ A e. H ) -> A e. ~H ) |