Metamath Proof Explorer


Theorem unitcl

Description: A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses unitcl.1 B=BaseR
unitcl.2 U=UnitR
Assertion unitcl XUXB

Proof

Step Hyp Ref Expression
1 unitcl.1 B=BaseR
2 unitcl.2 U=UnitR
3 eqid 1R=1R
4 eqid rR=rR
5 eqid opprR=opprR
6 eqid ropprR=ropprR
7 2 3 4 5 6 isunit XUXrR1RXropprR1R
8 7 simplbi XUXrR1R
9 1 4 dvdsrcl XrR1RXB
10 8 9 syl XUXB