Theorem spansneleqi

Description: Membership relation implied by equality of spans. (Contributed by NM, 6-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spansneleqi	$$⊢A\in \mathscr{H}\to \left(\mathrm{span}\left(\left\{A\right\}\right)=\mathrm{span}\left(\left\{B\right\}\right)\to A\in \mathrm{span}\left(\left\{B\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		spansnid	$$⊢A\in \mathscr{H}\to A\in \mathrm{span}\left(\left\{A\right\}\right)$$
2		eleq2	$$⊢\mathrm{span}\left(\left\{A\right\}\right)=\mathrm{span}\left(\left\{B\right\}\right)\to \left(A\in \mathrm{span}\left(\left\{A\right\}\right)\leftrightarrow A\in \mathrm{span}\left(\left\{B\right\}\right)\right)$$
3	1 2	syl5ibcom	$$⊢A\in \mathscr{H}\to \left(\mathrm{span}\left(\left\{A\right\}\right)=\mathrm{span}\left(\left\{B\right\}\right)\to A\in \mathrm{span}\left(\left\{B\right\}\right)\right)$$