Theorem subrgss 20464

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 2724	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20463	. . 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 1533   ∈ wcel 2098   ⊆ wss 3940  ‘cfv 6533  (class class class)co 7401  Basecbs 17143   ↾_s cress 17172  1_rcur 20076  Ringcrg 20128  SubRingcsubrg 20459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fv 6541  df-ov 7404  df-subrg 20461

This theorem is referenced by:  subrgsubg  20469  subrg1  20474  subrgsubm  20477  subrgdvds  20478  subrguss  20479  subrginv  20480  subrgdv  20481  subrgmre  20489  subsubrg  20490  issubdrg  20621  sdrgss  20634  sdrgacs  20642  subdrgint  20644  abvres  20672  sralmod  21033  cnsubrg  21289  issubassa3  21728  sraassab  21730  sraassa  21731  sraassaOLD  21732  aspid  21737  issubassa2  21754  resspsrbas  21845  resspsradd  21846  resspsrmul  21847  resspsrvsca  21848  mplassa  21891  ressmplbas2  21892  subrgascl  21937  subrgasclcl  21938  mplind  21941  evlsval2  21960  evlssca  21962  evlsscasrng  21970  mpfconst  21974  mpff  21977  mpfaddcl  21978  mpfmulcl  21979  mpfind  21980  ply1assa  22041  evls1val  22161  evls1rhm  22163  evls1sca  22164  evls1scasrng  22180  pf1f  22191  sranlm  24523  clmsscn  24928  cphreccllem  25028  cphdivcl  25032  cphabscl  25035  cphsqrtcl2  25036  cphsqrtcl3  25037  cphipcl  25041  4cphipval2  25092  resscdrg  25208  srabn  25210  plypf1  26066  dvply2g  26139  taylply2  26221  0ringsubrg  32847  fldgenssp  32874  idlinsubrg  33018  evls1fpws  33113  evls1vsca  33117  asclply1subcl  33127  sralvec  33151  lsssra  33154  drgext0g  33155  drgextvsca  33156  drgext0gsca  33157  drgextsubrg  33158  drgextlsp  33159  drgextgsum  33160  fedgmullem1  33193  fedgmullem2  33194  fedgmul  33195  extdggt0  33215  fldexttr  33216  extdg1id  33221  elirng  33230  irngss  33231  0ringirng  33233  evls1maplmhm  33240  ply1annnr  33244  imacrhmcl  41580  evlsval3  41620  evlsvvval  41624  evlsbagval  41627  evlsevl  41632  evlsmhpvvval  41656  mhphf  41658  mhphf2  41659  mhphf3  41660  cnsrexpcl  42396  fsumcnsrcl  42397  cnsrplycl  42398  rgspnid  42403  rngunsnply  42404