Theorem subrgss 20475

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 2729	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20474	. . 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 3905  ‘cfv 6486  (class class class)co 7353  Basecbs 17138   ↾_s cress 17159  1_rcur 20084  Ringcrg 20136  SubRingcsubrg 20472

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 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7356  df-subrg 20473

This theorem is referenced by:  subrgsubg  20480  subrg1  20485  subrgsubm  20488  subrgdvds  20489  subrguss  20490  subrginv  20491  subrgdv  20492  subrgmre  20500  subsubrg  20501  issubdrg  20683  sdrgss  20696  sdrgacs  20704  subdrgint  20706  abvres  20734  sralmod  21109  cnsubrg  21352  issubassa3  21791  sraassab  21793  sraassa  21794  sraassaOLD  21795  aspid  21800  issubassa2  21817  resspsrbas  21899  resspsradd  21900  resspsrmul  21901  resspsrvsca  21902  mplassa  21947  ressmplbas2  21950  subrgascl  21989  subrgasclcl  21990  mplind  21993  evlsval2  22010  evlssca  22012  evlsscasrng  22020  mpfconst  22024  mpff  22027  mpfaddcl  22028  mpfmulcl  22029  mpfind  22030  ply1assa  22100  evls1val  22223  evls1rhm  22225  evls1sca  22226  evls1scasrng  22242  pf1f  22253  evls1fpws  22272  evls1vsca  22276  asclply1subcl  22277  evls1maplmhm  22280  sranlm  24588  clmsscn  24995  cphreccllem  25094  cphdivcl  25098  cphabscl  25101  cphsqrtcl2  25102  cphsqrtcl3  25103  cphipcl  25107  4cphipval2  25158  resscdrg  25274  srabn  25276  plypf1  26133  dvply2g  26208  dvply2gOLD  26209  taylply2  26291  taylply2OLD  26292  elrgspn  33196  elrgspnsubrunlem1  33197  elrgspnsubrunlem2  33198  elrgspnsubrun  33199  0ringsubrg  33201  subrdom  33234  fldgenssp  33267  idlinsubrg  33378  ressply1evls1  33510  ressasclcl  33516  vr1nz  33535  sralvec  33557  lsssra  33560  drgext0g  33561  drgextvsca  33562  drgext0gsca  33563  drgextsubrg  33564  drgextlsp  33565  drgextgsum  33566  fedgmullem1  33601  fedgmullem2  33602  fedgmul  33603  extdggt0  33629  fldexttr  33630  extdg1id  33637  fldextrspunlsp  33645  fldextrspunlem1  33646  fldextrspunfld  33647  elirng  33657  irngss  33658  0ringirng  33660  ply1annnr  33669  imacrhmcl  42487  evlsval3  42532  evlsvvval  42536  evlsbagval  42539  evlsevl  42544  evlsmhpvvval  42568  mhphf  42570  mhphf2  42571  mhphf3  42572  cnsrexpcl  43138  fsumcnsrcl  43139  cnsrplycl  43140  rgspnid  43141  rngunsnply  43142