Theorem subrgss 20025

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 2738	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20024	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴)))
4	3	simprbi 497	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴))
5	4	simpld 495	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106   ⊆ wss 3887  ‘cfv 6433  (class class class)co 7275  Basecbs 16912   ↾_s cress 16941  1_rcur 19737  Ringcrg 19783  SubRingcsubrg 20020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-subrg 20022

This theorem is referenced by:  subrgsubg  20030  subrg1  20034  subrgsubm  20037  subrgdvds  20038  subrguss  20039  subrginv  20040  subrgdv  20041  subrgmre  20048  issubdrg  20049  subsubrg  20050  sdrgss  20065  sdrgacs  20069  subdrgint  20071  abvres  20099  sralmod  20457  cnsubrg  20658  issubassa3  21072  sraassa  21074  aspid  21079  issubassa2  21096  resspsrbas  21184  resspsradd  21185  resspsrmul  21186  resspsrvsca  21187  mplassa  21227  ressmplbas2  21228  subrgascl  21274  subrgasclcl  21275  mplind  21278  evlsval2  21297  evlssca  21299  evlsscasrng  21307  mpfconst  21311  mpff  21314  mpfaddcl  21315  mpfmulcl  21316  mpfind  21317  ply1assa  21370  evls1val  21486  evls1rhm  21488  evls1sca  21489  evls1scasrng  21505  pf1f  21516  sranlm  23848  clmsscn  24242  cphreccllem  24342  cphdivcl  24346  cphabscl  24349  cphsqrtcl2  24350  cphsqrtcl3  24351  cphipcl  24355  4cphipval2  24406  resscdrg  24522  srabn  24524  plypf1  25373  dvply2g  25445  taylply2  25527  idlinsubrg  31608  sralvec  31675  drgext0g  31677  drgextvsca  31678  drgext0gsca  31679  drgextsubrg  31680  drgextlsp  31681  drgextgsum  31682  fedgmullem1  31710  fedgmullem2  31711  fedgmul  31712  extdggt0  31732  fldexttr  31733  extdg1id  31738  selvval2lem4  40228  evlsval3  40272  evlsbagval  40275  mhphf  40285  mhphf2  40286  mhphf3  40287  cnsrexpcl  40990  fsumcnsrcl  40991  cnsrplycl  40992  rgspnid  40997  rngunsnply  40998