Theorem unitss 20393

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

Syntax hints:   = wceq 1550   ⊆ wss 3895  ‘cfv 6506  Basecbs 17217  Unitcui 20372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-rep 5217  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-iun 4941  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fv 6514  df-ov 7384  df-dvdsr 20374  df-unit 20375

This theorem is referenced by:  unitgrpbas  20399  unitgrpid  20402  unitsubm  20403  dvrdir  20429  rdivmuldivd  20430  invrpropd  20435  elrhmunit  20528  rhmunitinv  20529  fidomndrng  20791  issubdrg  20798  imadrhmcl  20815  znunithash  21585  dvrcn  24213  nmdvr  24699  nrginvrcnlem  24720  nrginvrcn  24721  dchrelbasd  27269  dchrinvcl  27283  dchrghm  27286  dchr1  27287  dchreq  27288  dchrresb  27289  dchrabs  27290  dchrinv  27291  dchrptlem1  27294  dchrptlem2  27295  dchrpt  27297  dchrsum2  27298  dchrsum  27299  sum2dchr  27304  lgsdchr  27385  rpvmasum2  27542  dvrcan5  33366  isdrng4  33428  dvdsruassoi  33516  lidlunitel  33555  assafld  33878  unitscyglem5  42754  aks5lem7  42755  idomodle  43706