Theorem subrgss 20572

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 20571	. . 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 1540   ∈ wcel 2108   ⊆ wss 3951  ‘cfv 6561  (class class class)co 7431  Basecbs 17247   ↾_s cress 17274  1_rcur 20178  Ringcrg 20230  SubRingcsubrg 20569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-subrg 20570

This theorem is referenced by:  subrgsubg  20577  subrg1  20582  subrgsubm  20585  subrgdvds  20586  subrguss  20587  subrginv  20588  subrgdv  20589  subrgmre  20597  subsubrg  20598  issubdrg  20781  sdrgss  20794  sdrgacs  20802  subdrgint  20804  abvres  20832  sralmod  21194  cnsubrg  21445  issubassa3  21886  sraassab  21888  sraassa  21889  sraassaOLD  21890  aspid  21895  issubassa2  21912  resspsrbas  21994  resspsradd  21995  resspsrmul  21996  resspsrvsca  21997  mplassa  22042  ressmplbas2  22045  subrgascl  22090  subrgasclcl  22091  mplind  22094  evlsval2  22111  evlssca  22113  evlsscasrng  22121  mpfconst  22125  mpff  22128  mpfaddcl  22129  mpfmulcl  22130  mpfind  22131  ply1assa  22201  evls1val  22324  evls1rhm  22326  evls1sca  22327  evls1scasrng  22343  pf1f  22354  evls1fpws  22373  evls1vsca  22377  asclply1subcl  22378  evls1maplmhm  22381  sranlm  24705  clmsscn  25112  cphreccllem  25212  cphdivcl  25216  cphabscl  25219  cphsqrtcl2  25220  cphsqrtcl3  25221  cphipcl  25225  4cphipval2  25276  resscdrg  25392  srabn  25394  plypf1  26251  dvply2g  26326  dvply2gOLD  26327  taylply2  26409  taylply2OLD  26410  elrgspn  33250  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  elrgspnsubrun  33253  0ringsubrg  33255  subrdom  33288  fldgenssp  33320  idlinsubrg  33459  ressasclcl  33596  sralvec  33636  lsssra  33639  drgext0g  33640  drgextvsca  33641  drgext0gsca  33642  drgextsubrg  33643  drgextlsp  33644  drgextgsum  33645  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  extdggt0  33708  fldexttr  33709  extdg1id  33716  fldextrspunlsp  33724  fldextrspunlem1  33725  fldextrspunfld  33726  elirng  33736  irngss  33737  0ringirng  33739  ply1annnr  33746  imacrhmcl  42524  evlsval3  42569  evlsvvval  42573  evlsbagval  42576  evlsevl  42581  evlsmhpvvval  42605  mhphf  42607  mhphf2  42608  mhphf3  42609  cnsrexpcl  43177  fsumcnsrcl  43178  cnsrplycl  43179  rgspnid  43180  rngunsnply  43181