Theorem unitss 20314

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

Syntax hints:   = wceq 1542   ⊆ wss 3890  ‘cfv 6490  Basecbs 17137  Unitcui 20293

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 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fv 6498  df-ov 7361  df-dvdsr 20295  df-unit 20296

This theorem is referenced by:  unitgrpbas  20320  unitgrpid  20323  unitsubm  20324  dvrdir  20350  rdivmuldivd  20351  invrpropd  20356  elrhmunit  20445  rhmunitinv  20446  fidomndrng  20708  issubdrg  20715  imadrhmcl  20732  znunithash  21521  dvrcn  24127  nmdvr  24613  nrginvrcnlem  24634  nrginvrcn  24635  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  33302  isdrng4  33361  dvdsruassoi  33449  lidlunitel  33488  assafld  33787  unitscyglem5  42630  aks5lem7  42631  idomodle  43622