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

Metamath Proof Explorer

Theorem spansnss2

Description: The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 16-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnss2 ⊢ A ∈ S ℋ ∧ B ∈ ℋ → B ∈ A ↔ span ⁡ B ⊆ A

Proof

Step Hyp Ref Expression
1 spansnss ⊢ A ∈ S ℋ ∧ B ∈ A → span ⁡ B ⊆ A
2 1 ex ⊢ A ∈ S ℋ → B ∈ A → span ⁡ B ⊆ A
3 2 adantr ⊢ A ∈ S ℋ ∧ B ∈ ℋ → B ∈ A → span ⁡ B ⊆ A
4 spansnid ⊢ B ∈ ℋ → B ∈ span ⁡ B
5 ssel ⊢ span ⁡ B ⊆ A → B ∈ span ⁡ B → B ∈ A
6 4 5 syl5com ⊢ B ∈ ℋ → span ⁡ B ⊆ A → B ∈ A
7 6 adantl ⊢ A ∈ S ℋ ∧ B ∈ ℋ → span ⁡ B ⊆ A → B ∈ A
8 3 7 impbid ⊢ A ∈ S ℋ ∧ B ∈ ℋ → B ∈ A ↔ span ⁡ B ⊆ A