Theorem unitss

Description: The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	unitcl.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	unitcl.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	unitss	⊢ 𝑈 ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		unitcl.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		unitcl.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3	1 2	unitcl	⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ∈ 𝐵 )
4	3	ssriv	⊢ 𝑈 ⊆ 𝐵