Theorem subrgss 20488

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 2730	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20487	. . 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 1540   ∈ wcel 2109   ⊆ wss 3917  ‘cfv 6514  (class class class)co 7390  Basecbs 17186   ↾_s cress 17207  1_rcur 20097  Ringcrg 20149  SubRingcsubrg 20485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-subrg 20486

This theorem is referenced by:  subrgsubg  20493  subrg1  20498  subrgsubm  20501  subrgdvds  20502  subrguss  20503  subrginv  20504  subrgdv  20505  subrgmre  20513  subsubrg  20514  issubdrg  20696  sdrgss  20709  sdrgacs  20717  subdrgint  20719  abvres  20747  sralmod  21101  cnsubrg  21351  issubassa3  21782  sraassab  21784  sraassa  21785  sraassaOLD  21786  aspid  21791  issubassa2  21808  resspsrbas  21890  resspsradd  21891  resspsrmul  21892  resspsrvsca  21893  mplassa  21938  ressmplbas2  21941  subrgascl  21980  subrgasclcl  21981  mplind  21984  evlsval2  22001  evlssca  22003  evlsscasrng  22011  mpfconst  22015  mpff  22018  mpfaddcl  22019  mpfmulcl  22020  mpfind  22021  ply1assa  22091  evls1val  22214  evls1rhm  22216  evls1sca  22217  evls1scasrng  22233  pf1f  22244  evls1fpws  22263  evls1vsca  22267  asclply1subcl  22268  evls1maplmhm  22271  sranlm  24579  clmsscn  24986  cphreccllem  25085  cphdivcl  25089  cphabscl  25092  cphsqrtcl2  25093  cphsqrtcl3  25094  cphipcl  25098  4cphipval2  25149  resscdrg  25265  srabn  25267  plypf1  26124  dvply2g  26199  dvply2gOLD  26200  taylply2  26282  taylply2OLD  26283  elrgspn  33204  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  elrgspnsubrun  33207  0ringsubrg  33209  subrdom  33242  fldgenssp  33275  idlinsubrg  33409  ressply1evls1  33541  ressasclcl  33547  vr1nz  33566  sralvec  33588  lsssra  33591  drgext0g  33592  drgextvsca  33593  drgext0gsca  33594  drgextsubrg  33595  drgextlsp  33596  drgextgsum  33597  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  extdggt0  33660  fldexttr  33661  extdg1id  33668  fldextrspunlsp  33676  fldextrspunlem1  33677  fldextrspunfld  33678  elirng  33688  irngss  33689  0ringirng  33691  ply1annnr  33700  imacrhmcl  42509  evlsval3  42554  evlsvvval  42558  evlsbagval  42561  evlsevl  42566  evlsmhpvvval  42590  mhphf  42592  mhphf2  42593  mhphf3  42594  cnsrexpcl  43161  fsumcnsrcl  43162  cnsrplycl  43163  rgspnid  43164  rngunsnply  43165