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	$$⊢B={\mathrm{Base}}_R$$
	unitcl.2	$$⊢U=\mathrm{Unit}\left(R\right)$$
Assertion	unitss	$$⊢U\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		unitcl.1	$$⊢B={\mathrm{Base}}_R$$
2		unitcl.2	$$⊢U=\mathrm{Unit}\left(R\right)$$
3	1 2	unitcl	$$⊢x\in U\to x\in B$$
4	3	ssriv	$$⊢U\subseteq B$$