MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unitss Structured version   Visualization version   GIF version

Theorem unitss 19703
Description: The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.)
Hypotheses
Ref Expression
unitcl.1 𝐵 = (Base‘𝑅)
unitcl.2 𝑈 = (Unit‘𝑅)
Assertion
Ref Expression
unitss 𝑈𝐵

Proof of Theorem unitss
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 unitcl.1 . . 3 𝐵 = (Base‘𝑅)
2 unitcl.2 . . 3 𝑈 = (Unit‘𝑅)
31, 2unitcl 19702 . 2 (𝑥𝑈𝑥𝐵)
43ssriv 3920 1 𝑈𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  wss 3881  cfv 6398  Basecbs 16785  Unitcui 19682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5194  ax-sep 5207  ax-nul 5214  ax-pow 5273  ax-pr 5337  ax-un 7542
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3423  df-sbc 3710  df-csb 3827  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4253  df-if 4455  df-pw 4530  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4835  df-iun 4921  df-br 5069  df-opab 5131  df-mpt 5151  df-id 5470  df-xp 5572  df-rel 5573  df-cnv 5574  df-co 5575  df-dm 5576  df-rn 5577  df-res 5578  df-ima 5579  df-iota 6356  df-fun 6400  df-fn 6401  df-f 6402  df-f1 6403  df-fo 6404  df-f1o 6405  df-fv 6406  df-ov 7235  df-dvdsr 19684  df-unit 19685
This theorem is referenced by:  unitgrpbas  19709  unitgrpid  19712  unitsubm  19713  invrpropd  19741  issubdrg  19850  fidomndrng  20370  znunithash  20554  dvrcn  23105  nmdvr  23592  nrginvrcnlem  23613  nrginvrcn  23614  dchrelbasd  26144  dchrinvcl  26158  dchrghm  26161  dchr1  26162  dchreq  26163  dchrresb  26164  dchrabs  26165  dchrinv  26166  dchrptlem1  26169  dchrptlem2  26170  dchrpt  26172  dchrsum2  26173  dchrsum  26174  sum2dchr  26179  lgsdchr  26260  rpvmasum2  26417  dvrdir  31230  rdivmuldivd  31231  dvrcan5  31233  elrhmunit  31262  rhmunitinv  31264  idomodle  40753
  Copyright terms: Public domain W3C validator