Theorem subrgss 20500

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 2727	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20499	. . 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 1534   ∈ wcel 2099   ⊆ wss 3944  ‘cfv 6542  (class class class)co 7414  Basecbs 17171   ↾_s cress 17200  1_rcur 20112  Ringcrg 20164  SubRingcsubrg 20495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-ov 7417  df-subrg 20497

This theorem is referenced by:  subrgsubg  20505  subrg1  20510  subrgsubm  20513  subrgdvds  20514  subrguss  20515  subrginv  20516  subrgdv  20517  subrgmre  20525  subsubrg  20526  issubdrg  20657  sdrgss  20670  sdrgacs  20678  subdrgint  20680  abvres  20708  sralmod  21069  cnsubrg  21347  issubassa3  21786  sraassab  21788  sraassa  21789  sraassaOLD  21790  aspid  21795  issubassa2  21812  resspsrbas  21904  resspsradd  21905  resspsrmul  21906  resspsrvsca  21907  mplassa  21951  ressmplbas2  21952  subrgascl  21997  subrgasclcl  21998  mplind  22001  evlsval2  22020  evlssca  22022  evlsscasrng  22030  mpfconst  22034  mpff  22037  mpfaddcl  22038  mpfmulcl  22039  mpfind  22040  ply1assa  22105  evls1val  22226  evls1rhm  22228  evls1sca  22229  evls1scasrng  22245  pf1f  22256  sranlm  24588  clmsscn  24993  cphreccllem  25093  cphdivcl  25097  cphabscl  25100  cphsqrtcl2  25101  cphsqrtcl3  25102  cphipcl  25106  4cphipval2  25157  resscdrg  25273  srabn  25275  plypf1  26133  dvply2g  26206  dvply2gOLD  26207  taylply2  26289  taylply2OLD  26290  0ringsubrg  32917  fldgenssp  32945  idlinsubrg  33082  evls1fpws  33182  evls1vsca  33187  asclply1subcl  33193  sralvec  33217  lsssra  33220  drgext0g  33221  drgextvsca  33222  drgext0gsca  33223  drgextsubrg  33224  drgextlsp  33225  drgextgsum  33226  fedgmullem1  33259  fedgmullem2  33260  fedgmul  33261  extdggt0  33281  fldexttr  33282  extdg1id  33287  elirng  33296  irngss  33297  0ringirng  33299  evls1maplmhm  33306  ply1annnr  33310  imacrhmcl  41673  evlsval3  41714  evlsvvval  41718  evlsbagval  41721  evlsevl  41726  evlsmhpvvval  41750  mhphf  41752  mhphf2  41753  mhphf3  41754  cnsrexpcl  42511  fsumcnsrcl  42512  cnsrplycl  42513  rgspnid  42518  rngunsnply  42519