Theorem subrgss 20510

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 20509	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴)))
4	3	simprbi 496	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴))
5	4	simpld 494	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ⊆ wss 3902  ‘cfv 6493  (class class class)co 7361  Basecbs 17141   ↾_s cress 17162  1_rcur 20121  Ringcrg 20173  SubRingcsubrg 20507

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 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fv 6501  df-ov 7364  df-subrg 20508

This theorem is referenced by:  subrgsubg  20515  subrg1  20520  subrgsubm  20523  subrgdvds  20524  subrguss  20525  subrginv  20526  subrgdv  20527  subrgmre  20535  subsubrg  20536  issubdrg  20718  sdrgss  20731  sdrgacs  20739  subdrgint  20741  abvres  20769  sralmod  21144  cnsubrg  21387  issubassa3  21826  sraassab  21828  sraassa  21829  sraassaOLD  21830  aspid  21835  issubassa2  21853  resspsrbas  21934  resspsradd  21935  resspsrmul  21936  resspsrvsca  21937  mplassa  21982  ressmplbas2  21987  subrgascl  22026  subrgasclcl  22027  mplind  22030  evlsval2  22047  evlsval3  22049  evlsvvval  22053  evlssca  22054  evlsscasrng  22065  mpfconst  22069  mpff  22072  mpfaddcl  22073  mpfmulcl  22074  mpfind  22075  ply1assa  22145  evls1val  22269  evls1rhm  22271  evls1sca  22272  evls1scasrng  22288  pf1f  22299  evls1fpws  22318  evls1vsca  22322  asclply1subcl  22323  evls1maplmhm  22326  sranlm  24633  clmsscn  25040  cphreccllem  25139  cphdivcl  25143  cphabscl  25146  cphsqrtcl2  25147  cphsqrtcl3  25148  cphipcl  25152  4cphipval2  25203  resscdrg  25319  srabn  25321  plypf1  26178  dvply2g  26253  dvply2gOLD  26254  taylply2  26336  taylply2OLD  26337  elrgspn  33332  elrgspnsubrunlem1  33333  elrgspnsubrunlem2  33334  elrgspnsubrun  33335  0ringsubrg  33337  subrdom  33371  fldgenssp  33404  idlinsubrg  33516  ressply1evls1  33650  ressasclcl  33656  vr1nz  33678  sralvec  33754  lsssra  33757  drgext0g  33759  drgextvsca  33760  drgext0gsca  33761  drgextsubrg  33762  drgextlsp  33763  drgextgsum  33764  fedgmullem1  33799  fedgmullem2  33800  fedgmul  33801  extdggt0  33827  fldexttr  33828  extdg1id  33836  fldextrspunlsp  33844  fldextrspunlem1  33845  fldextrspunfld  33846  elirng  33856  irngss  33857  0ringirng  33859  ply1annnr  33873  imacrhmcl  42847  evlsbagval  42890  evlsevl  42895  evlsmhpvvval  42916  mhphf  42918  mhphf2  42919  mhphf3  42920  cnsrexpcl  43485  fsumcnsrcl  43486  cnsrplycl  43487  rgspnid  43488  rngunsnply  43489