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 = ( Base ` R )
	unitcl.2	|- U = ( Unit ` R )
Assertion	unitss	|- U C_ B

Proof

Step	Hyp	Ref	Expression
1		unitcl.1	|- B = ( Base ` R )
2		unitcl.2	|- U = ( Unit ` R )
3	1 2	unitcl	|- ( x e. U -> x e. B )
4	3	ssriv	|- U C_ B