Theorem unitss 20435

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

Syntax hints:   = wceq 1561   ⊆ wss 3905  ‘cfv 6521  Basecbs 17255  Unitcui 20414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fv 6529  df-ov 7399  df-dvdsr 20416  df-unit 20417

This theorem is referenced by:  unitgrpbas  20441  unitgrpid  20444  unitsubm  20445  dvrdir  20471  rdivmuldivd  20472  invrpropd  20477  elrhmunit  20570  rhmunitinv  20571  fidomndrng  20830  issubdrg  20836  imadrhmcl  20853  znunithash  21623  dvrcn  24251  nmdvr  24737  nrginvrcnlem  24758  nrginvrcn  24759  dchrelbasd  27310  dchrinvcl  27324  dchrghm  27327  dchr1  27328  dchreq  27329  dchrresb  27330  dchrabs  27331  dchrinv  27332  dchrptlem1  27335  dchrptlem2  27336  dchrpt  27338  dchrsum2  27339  dchrsum  27340  sum2dchr  27345  lgsdchr  27426  rpvmasum2  27583  dvrcan5  33422  isdrng4  33485  dvdsruassoi  33573  lidlunitel  33612  assafld  33936  unitscyglem5  42821  aks5lem7  42822  idomodle  43773