Theorem subrgss 20493

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 2731	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20492	. . 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 1541   ∈ wcel 2111   ⊆ wss 3897  ‘cfv 6487  (class class class)co 7352  Basecbs 17126   ↾_s cress 17147  1_rcur 20105  Ringcrg 20157  SubRingcsubrg 20490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fv 6495  df-ov 7355  df-subrg 20491

This theorem is referenced by:  subrgsubg  20498  subrg1  20503  subrgsubm  20506  subrgdvds  20507  subrguss  20508  subrginv  20509  subrgdv  20510  subrgmre  20518  subsubrg  20519  issubdrg  20701  sdrgss  20714  sdrgacs  20722  subdrgint  20724  abvres  20752  sralmod  21127  cnsubrg  21370  issubassa3  21809  sraassab  21811  sraassa  21812  sraassaOLD  21813  aspid  21818  issubassa2  21835  resspsrbas  21917  resspsradd  21918  resspsrmul  21919  resspsrvsca  21920  mplassa  21965  ressmplbas2  21968  subrgascl  22007  subrgasclcl  22008  mplind  22011  evlsval2  22028  evlssca  22030  evlsscasrng  22038  mpfconst  22042  mpff  22045  mpfaddcl  22046  mpfmulcl  22047  mpfind  22048  ply1assa  22118  evls1val  22241  evls1rhm  22243  evls1sca  22244  evls1scasrng  22260  pf1f  22271  evls1fpws  22290  evls1vsca  22294  asclply1subcl  22295  evls1maplmhm  22298  sranlm  24605  clmsscn  25012  cphreccllem  25111  cphdivcl  25115  cphabscl  25118  cphsqrtcl2  25119  cphsqrtcl3  25120  cphipcl  25124  4cphipval2  25175  resscdrg  25291  srabn  25293  plypf1  26150  dvply2g  26225  dvply2gOLD  26226  taylply2  26308  taylply2OLD  26309  elrgspn  33220  elrgspnsubrunlem1  33221  elrgspnsubrunlem2  33222  elrgspnsubrun  33223  0ringsubrg  33225  subrdom  33258  fldgenssp  33291  idlinsubrg  33403  ressply1evls1  33535  ressasclcl  33541  vr1nz  33561  sralvec  33604  lsssra  33607  drgext0g  33609  drgextvsca  33610  drgext0gsca  33611  drgextsubrg  33612  drgextlsp  33613  drgextgsum  33614  fedgmullem1  33649  fedgmullem2  33650  fedgmul  33651  extdggt0  33677  fldexttr  33678  extdg1id  33686  fldextrspunlsp  33694  fldextrspunlem1  33695  fldextrspunfld  33696  elirng  33706  irngss  33707  0ringirng  33709  ply1annnr  33723  imacrhmcl  42613  evlsval3  42658  evlsvvval  42662  evlsbagval  42665  evlsevl  42670  evlsmhpvvval  42694  mhphf  42696  mhphf2  42697  mhphf3  42698  cnsrexpcl  43263  fsumcnsrcl  43264  cnsrplycl  43265  rgspnid  43266  rngunsnply  43267