Theorem elspansni

Description: Membership in the span of a singleton. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypothesis	spansn.1	|- A e. ~H
Assertion	elspansni	|- ( B e. ( span ` { A } ) <-> E. x e. CC B = ( x .h A ) )

Proof

Step	Hyp	Ref	Expression
1		spansn.1	|- A e. ~H
2	1	spansni	|- ( span ` { A } ) = ( _|_ ` ( _|_ ` { A } ) )
3	2	eleq2i	|- ( B e. ( span ` { A } ) <-> B e. ( _|_ ` ( _|_ ` { A } ) ) )
4	1	h1de2ci	|- ( B e. ( _|_ ` ( _|_ ` { A } ) ) <-> E. x e. CC B = ( x .h A ) )
5	3 4	bitri	|- ( B e. ( span ` { A } ) <-> E. x e. CC B = ( x .h A ) )