This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℋ \land B \in span (\{A\})) \to B \in ℋ$

Step	Hyp	Ref	Expression
1		snssi	$⊢ A \in ℋ \to \{A\} \subseteq ℋ$
2		elspancl	$⊢ (\{A\} \subseteq ℋ \land B \in span (\{A\})) \to B \in ℋ$
3	1 2	sylan	$⊢ (A \in ℋ \land B \in span (\{A\})) \to B \in ℋ$