Theorem subrgss 20656

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568   ∈ wcel 2141   ⊆ wss 3904  ‘cfv 6536  (class class class)co 7410  Basecbs 17268   ↾_s cress 17289  1_rcur 20262  Ringcrg 20314  SubRingcsubrg 20653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fv 6544  df-ov 7413  df-subrg 20654

This theorem is referenced by:  subrgsubg  20661  subrg1  20666  subrgsubm  20669  subrgdvds  20670  subrguss  20671  subrginv  20672  subrgdv  20673  subrgmre  20681  subsubrg  20682  issubdrg  20862  sdrgss  20875  sdrgacs  20883  subdrgint  20885  abvres  20913  sralmod  21287  cnsubrg  21556  issubassa3  21995  sraassab  21997  sraassa  21998  aspid  22003  issubassa2  22021  resspsrbas  22102  resspsradd  22103  resspsrmul  22104  resspsrvsca  22105  mplassa  22150  ressmplbas2  22156  subrgascl  22196  subrgasclcl  22197  mplind  22200  evlsval2  22217  evlsval3  22219  evlsvvval  22223  evlssca  22224  evlsscasrng  22235  mpfconst  22239  mpff  22242  mpfaddcl  22243  mpfmulcl  22244  mpfind  22245  evlsevl  22262  ply1assa  22338  evls1val  22459  evls1rhm  22461  evls1sca  22462  evls1scasrng  22478  pf1f  22489  evls1fpws  22508  evls1vsca  22512  asclply1subcl  22513  evls1maplmhm  22516  sranlm  24820  clmsscn  25217  cphreccllem  25316  cphdivcl  25320  cphabscl  25323  cphsqrtcl2  25324  cphsqrtcl3  25325  cphipcl  25329  4cphipval2  25380  resscdrg  25496  srabn  25498  plypf1  26348  dvply2g  26425  taylply2  26507  elrgspn  33532  elrgspnsubrunlem1  33533  elrgspnsubrunlem2  33534  elrgspnsubrun  33535  0ringsubrg  33537  subrdom  33571  fldgenssp  33605  idlinsubrg  33705  ressply1evls1  33821  ressasclcl  33827  vr1nz  33849  sralvec  33941  lsssra  33944  drgext0g  33946  drgextvsca  33947  drgext0gsca  33948  drgextsubrg  33949  drgextlsp  33950  drgextgsum  33951  fedgmullem1  33985  fedgmullem2  33986  fedgmul  33987  extdggt0  34013  fldexttr  34014  extdg1id  34022  fldextrspunlsp  34030  fldextrspunlem1  34031  fldextrspunfld  34032  elirng  34042  irngss  34043  0ringirng  34045  ply1annnr  34059  imacrhmcl  43234  evlsbagval  43266  evlsmhpvvval  43275  mhphf  43277  mhphf2  43278  mhphf3  43279  cnsrexpcl  43840  fsumcnsrcl  43841  cnsrplycl  43842  rgspnid  43843  rngunsnply  43844