Theorem subrgss 20462

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 2732	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20461	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴)))
4	3	simprbi 497	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴))
5	4	simpld 495	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ⊆ wss 3948  ‘cfv 6543  (class class class)co 7411  Basecbs 17148   ↾_s cress 17177  1_rcur 20075  Ringcrg 20127  SubRingcsubrg 20457

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7414  df-subrg 20459

This theorem is referenced by:  subrgsubg  20467  subrg1  20472  subrgsubm  20475  subrgdvds  20476  subrguss  20477  subrginv  20478  subrgdv  20479  subrgmre  20487  subsubrg  20488  issubdrg  20544  sdrgss  20552  sdrgacs  20560  subdrgint  20562  abvres  20590  sralmod  20954  cnsubrg  21205  issubassa3  21639  sraassab  21641  sraassa  21642  sraassaOLD  21643  aspid  21648  issubassa2  21665  resspsrbas  21754  resspsradd  21755  resspsrmul  21756  resspsrvsca  21757  mplassa  21800  ressmplbas2  21801  subrgascl  21846  subrgasclcl  21847  mplind  21850  evlsval2  21869  evlssca  21871  evlsscasrng  21879  mpfconst  21883  mpff  21886  mpfaddcl  21887  mpfmulcl  21888  mpfind  21889  ply1assa  21942  evls1val  22059  evls1rhm  22061  evls1sca  22062  evls1scasrng  22078  pf1f  22089  sranlm  24421  clmsscn  24819  cphreccllem  24919  cphdivcl  24923  cphabscl  24926  cphsqrtcl2  24927  cphsqrtcl3  24928  cphipcl  24932  4cphipval2  24983  resscdrg  25099  srabn  25101  plypf1  25950  dvply2g  26022  taylply2  26104  0ringsubrg  32637  fldgenssp  32666  idlinsubrg  32811  evls1fpws  32908  evls1vsca  32912  asclply1subcl  32922  sralvec  32948  lsssra  32951  drgext0g  32952  drgextvsca  32953  drgext0gsca  32954  drgextsubrg  32955  drgextlsp  32956  drgextgsum  32957  fedgmullem1  32990  fedgmullem2  32991  fedgmul  32992  extdggt0  33012  fldexttr  33013  extdg1id  33018  elirng  33027  irngss  33028  0ringirng  33030  evls1maplmhm  33037  ply1annnr  33041  imacrhmcl  41393  evlsval3  41433  evlsvvval  41437  evlsbagval  41440  evlsevl  41445  evlsmhpvvval  41469  mhphf  41471  mhphf2  41472  mhphf3  41473  cnsrexpcl  42209  fsumcnsrcl  42210  cnsrplycl  42211  rgspnid  42216  rngunsnply  42217