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 B span A B

Proof

Step Hyp Ref Expression
1 snssi A A
2 elspancl A B span A B
3 1 2 sylan A B span A B