Theorem spansneleqi

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

	Ref	Expression
Assertion	spansneleqi	⊢ ( 𝐴 ∈ ℋ → ( ( span ‘ { 𝐴 } ) = ( span ‘ { 𝐵 } ) → 𝐴 ∈ ( span ‘ { 𝐵 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		spansnid	⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( span ‘ { 𝐴 } ) )
2		eleq2	⊢ ( ( span ‘ { 𝐴 } ) = ( span ‘ { 𝐵 } ) → ( 𝐴 ∈ ( span ‘ { 𝐴 } ) ↔ 𝐴 ∈ ( span ‘ { 𝐵 } ) ) )
3	1 2	syl5ibcom	⊢ ( 𝐴 ∈ ℋ → ( ( span ‘ { 𝐴 } ) = ( span ‘ { 𝐵 } ) → 𝐴 ∈ ( span ‘ { 𝐵 } ) ) )