Metamath Proof Explorer


Theorem spansnid

Description: A vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnid A A span A

Proof

Step Hyp Ref Expression
1 h1did A A A
2 spansn A span A = A
3 1 2 eleqtrrd A A span A