Theorem unitss 20345

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.

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

Syntax hints:   = wceq 1542   ⊆ wss 3885  ‘cfv 6487  Basecbs 17168  Unitcui 20324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fv 6495  df-ov 7359  df-dvdsr 20326  df-unit 20327

This theorem is referenced by:  unitgrpbas  20351  unitgrpid  20354  unitsubm  20355  dvrdir  20381  rdivmuldivd  20382  invrpropd  20387  elrhmunit  20476  rhmunitinv  20477  fidomndrng  20739  issubdrg  20746  imadrhmcl  20763  znunithash  21533  dvrcn  24137  nmdvr  24623  nrginvrcnlem  24644  nrginvrcn  24645  dchrelbasd  27190  dchrinvcl  27204  dchrghm  27207  dchr1  27208  dchreq  27209  dchrresb  27210  dchrabs  27211  dchrinv  27212  dchrptlem1  27215  dchrptlem2  27216  dchrpt  27218  dchrsum2  27219  dchrsum  27220  sum2dchr  27225  lgsdchr  27306  rpvmasum2  27463  dvrcan5  33285  isdrng4  33344  dvdsruassoi  33432  lidlunitel  33471  assafld  33769  unitscyglem5  42626  aks5lem7  42627  idomodle  43607