Metamath Proof Explorer

Theorem elspansncl

Description: A member of a span of a singleton is a vector. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion elspansncl 
|- ( ( A e. ~H /\ B e. ( span ` { A } ) ) -> B e. ~H )

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( A e. ~H -> { A } C_ ~H )
2 elspancl 
 |-  ( ( { A } C_ ~H /\ B e. ( span ` { A } ) ) -> B e. ~H )
3 1 2 sylan 
 |-  ( ( A e. ~H /\ B e. ( span ` { A } ) ) -> B e. ~H )