Theorem subrgss 20507

Description: A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)

Hypothesis

Ref	Expression
subrgss.1	⊢ 𝐵 = (Base‘𝑅)

Assertion

Ref	Expression
subrgss	⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵)

Proof of Theorem subrgss

Step	Hyp	Ref	Expression
1		subrgss.1	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
2		eqid 2737	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20506	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴)))
4	3	simprbi 497	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴))
5	4	simpld 494	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  ‘cfv 6490  (class class class)co 7358  Basecbs 17137   ↾_s cress 17158  1_rcur 20120  Ringcrg 20172  SubRingcsubrg 20504

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-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368

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-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-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-subrg 20505

This theorem is referenced by:  subrgsubg  20512  subrg1  20517  subrgsubm  20520  subrgdvds  20521  subrguss  20522  subrginv  20523  subrgdv  20524  subrgmre  20532  subsubrg  20533  issubdrg  20715  sdrgss  20728  sdrgacs  20736  subdrgint  20738  abvres  20766  sralmod  21141  cnsubrg  21384  issubassa3  21823  sraassab  21825  sraassa  21826  aspid  21831  issubassa2  21849  resspsrbas  21930  resspsradd  21931  resspsrmul  21932  resspsrvsca  21933  mplassa  21978  ressmplbas2  21983  subrgascl  22022  subrgasclcl  22023  mplind  22026  evlsval2  22043  evlsval3  22045  evlsvvval  22049  evlssca  22050  evlsscasrng  22061  mpfconst  22065  mpff  22068  mpfaddcl  22069  mpfmulcl  22070  mpfind  22071  ply1assa  22141  evls1val  22263  evls1rhm  22265  evls1sca  22266  evls1scasrng  22282  pf1f  22293  evls1fpws  22312  evls1vsca  22316  asclply1subcl  22317  evls1maplmhm  22320  sranlm  24627  clmsscn  25024  cphreccllem  25123  cphdivcl  25127  cphabscl  25130  cphsqrtcl2  25131  cphsqrtcl3  25132  cphipcl  25136  4cphipval2  25187  resscdrg  25303  srabn  25305  plypf1  26158  dvply2g  26232  dvply2gOLD  26233  taylply2  26315  taylply2OLD  26316  elrgspn  33312  elrgspnsubrunlem1  33313  elrgspnsubrunlem2  33314  elrgspnsubrun  33315  0ringsubrg  33317  subrdom  33351  fldgenssp  33384  idlinsubrg  33496  ressply1evls1  33630  ressasclcl  33636  vr1nz  33658  sralvec  33734  lsssra  33737  drgext0g  33739  drgextvsca  33740  drgext0gsca  33741  drgextsubrg  33742  drgextlsp  33743  drgextgsum  33744  fedgmullem1  33779  fedgmullem2  33780  fedgmul  33781  extdggt0  33807  fldexttr  33808  extdg1id  33816  fldextrspunlsp  33824  fldextrspunlem1  33825  fldextrspunfld  33826  elirng  33836  irngss  33837  0ringirng  33839  ply1annnr  33853  imacrhmcl  42958  evlsbagval  43001  evlsevl  43006  evlsmhpvvval  43027  mhphf  43029  mhphf2  43030  mhphf3  43031  cnsrexpcl  43596  fsumcnsrcl  43597  cnsrplycl  43598  rgspnid  43599  rngunsnply  43600