Metamath Proof Explorer


Theorem elspancl

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

Ref Expression
Assertion elspancl A B span A B

Proof

Step Hyp Ref Expression
1 spancl A span A S
2 shel span A S B span A B
3 1 2 sylan A B span A B