Theorem subrgss 20549

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 20548	. . 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 6499  (class class class)co 7367  Basecbs 17179   ↾_s cress 17200  1_rcur 20162  Ringcrg 20214  SubRingcsubrg 20546

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 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376

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 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6455  df-fun 6501  df-fv 6507  df-ov 7370  df-subrg 20547

This theorem is referenced by:  subrgsubg  20554  subrg1  20559  subrgsubm  20562  subrgdvds  20563  subrguss  20564  subrginv  20565  subrgdv  20566  subrgmre  20574  subsubrg  20575  issubdrg  20757  sdrgss  20770  sdrgacs  20778  subdrgint  20780  abvres  20808  sralmod  21182  cnsubrg  21407  issubassa3  21846  sraassab  21848  sraassa  21849  aspid  21854  issubassa2  21872  resspsrbas  21952  resspsradd  21953  resspsrmul  21954  resspsrvsca  21955  mplassa  22000  ressmplbas2  22005  subrgascl  22044  subrgasclcl  22045  mplind  22048  evlsval2  22065  evlsval3  22067  evlsvvval  22071  evlssca  22072  evlsscasrng  22083  mpfconst  22087  mpff  22090  mpfaddcl  22091  mpfmulcl  22092  mpfind  22093  ply1assa  22163  evls1val  22285  evls1rhm  22287  evls1sca  22288  evls1scasrng  22304  pf1f  22315  evls1fpws  22334  evls1vsca  22338  asclply1subcl  22339  evls1maplmhm  22342  sranlm  24649  clmsscn  25046  cphreccllem  25145  cphdivcl  25149  cphabscl  25152  cphsqrtcl2  25153  cphsqrtcl3  25154  cphipcl  25158  4cphipval2  25209  resscdrg  25325  srabn  25327  plypf1  26177  dvply2g  26251  taylply2  26333  elrgspn  33307  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  0ringsubrg  33312  subrdom  33346  fldgenssp  33379  idlinsubrg  33491  ressply1evls1  33625  ressasclcl  33631  vr1nz  33653  sralvec  33729  lsssra  33732  drgext0g  33734  drgextvsca  33735  drgext0gsca  33736  drgextsubrg  33737  drgextlsp  33738  drgextgsum  33739  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  extdggt0  33801  fldexttr  33802  extdg1id  33810  fldextrspunlsp  33818  fldextrspunlem1  33819  fldextrspunfld  33820  elirng  33830  irngss  33831  0ringirng  33833  ply1annnr  33847  imacrhmcl  42959  evlsbagval  43002  evlsevl  43007  evlsmhpvvval  43028  mhphf  43030  mhphf2  43031  mhphf3  43032  cnsrexpcl  43593  fsumcnsrcl  43594  cnsrplycl  43595  rgspnid  43596  rngunsnply  43597