Theorem subgss

Description: A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypothesis	issubg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	subgss	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		issubg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2	1	issubg	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ) )
3	2	simp2bi	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝐵 )