Theorem subrgss 20538

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 2735	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20537	. . 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 3885  ‘cfv 6487  (class class class)co 7356  Basecbs 17168   ↾_s cress 17189  1_rcur 20151  Ringcrg 20203  SubRingcsubrg 20535

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 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fv 6495  df-ov 7359  df-subrg 20536

This theorem is referenced by:  subrgsubg  20543  subrg1  20548  subrgsubm  20551  subrgdvds  20552  subrguss  20553  subrginv  20554  subrgdv  20555  subrgmre  20563  subsubrg  20564  issubdrg  20746  sdrgss  20759  sdrgacs  20767  subdrgint  20769  abvres  20797  sralmod  21171  cnsubrg  21396  issubassa3  21835  sraassab  21837  sraassa  21838  aspid  21843  issubassa2  21861  resspsrbas  21941  resspsradd  21942  resspsrmul  21943  resspsrvsca  21944  mplassa  21989  ressmplbas2  21994  subrgascl  22033  subrgasclcl  22034  mplind  22037  evlsval2  22054  evlsval3  22056  evlsvvval  22060  evlssca  22061  evlsscasrng  22072  mpfconst  22076  mpff  22079  mpfaddcl  22080  mpfmulcl  22081  mpfind  22082  ply1assa  22151  evls1val  22273  evls1rhm  22275  evls1sca  22276  evls1scasrng  22292  pf1f  22303  evls1fpws  22322  evls1vsca  22326  asclply1subcl  22327  evls1maplmhm  22330  sranlm  24637  clmsscn  25034  cphreccllem  25133  cphdivcl  25137  cphabscl  25140  cphsqrtcl2  25141  cphsqrtcl3  25142  cphipcl  25146  4cphipval2  25197  resscdrg  25313  srabn  25315  plypf1  26165  dvply2g  26239  taylply2  26321  elrgspn  33295  elrgspnsubrunlem1  33296  elrgspnsubrunlem2  33297  elrgspnsubrun  33298  0ringsubrg  33300  subrdom  33334  fldgenssp  33367  idlinsubrg  33479  ressply1evls1  33613  ressasclcl  33619  vr1nz  33641  sralvec  33717  lsssra  33720  drgext0g  33722  drgextvsca  33723  drgext0gsca  33724  drgextsubrg  33725  drgextlsp  33726  drgextgsum  33727  fedgmullem1  33761  fedgmullem2  33762  fedgmul  33763  extdggt0  33789  fldexttr  33790  extdg1id  33798  fldextrspunlsp  33806  fldextrspunlem1  33807  fldextrspunfld  33808  elirng  33818  irngss  33819  0ringirng  33821  ply1annnr  33835  imacrhmcl  42947  evlsbagval  42990  evlsevl  42995  evlsmhpvvval  43016  mhphf  43018  mhphf2  43019  mhphf3  43020  cnsrexpcl  43581  fsumcnsrcl  43582  cnsrplycl  43583  rgspnid  43584  rngunsnply  43585