Theorem unitss 20248

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 20247	. 2 ⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ 𝐵)
4	3	ssriv 3935	1 ⊢ 𝑈 ⊆ 𝐵

Syntax hints:   = wceq 1540   ⊆ wss 3899  ‘cfv 6476  Basecbs 17107  Unitcui 20227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5214  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5367  ax-un 7662

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3393  df-v 3435  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4940  df-br 5089  df-opab 5151  df-mpt 5170  df-id 5508  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-iota 6432  df-fun 6478  df-fv 6484  df-ov 7343  df-dvdsr 20229  df-unit 20230

This theorem is referenced by:  unitgrpbas  20254  unitgrpid  20257  unitsubm  20258  dvrdir  20284  rdivmuldivd  20285  invrpropd  20290  elrhmunit  20379  rhmunitinv  20380  fidomndrng  20642  issubdrg  20649  imadrhmcl  20666  znunithash  21455  dvrcn  24053  nmdvr  24539  nrginvrcnlem  24560  nrginvrcn  24561  dchrelbasd  27131  dchrinvcl  27145  dchrghm  27148  dchr1  27149  dchreq  27150  dchrresb  27151  dchrabs  27152  dchrinv  27153  dchrptlem1  27156  dchrptlem2  27157  dchrpt  27159  dchrsum2  27160  dchrsum  27161  sum2dchr  27166  lgsdchr  27247  rpvmasum2  27404  dvrcan5  33171  isdrng4  33229  dvdsruassoi  33317  lidlunitel  33356  assafld  33618  unitscyglem5  42189  aks5lem7  42190  idomodle  43181