Theorem subrgss 20532

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 2735	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20531	. . 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 2108   ⊆ wss 3926  ‘cfv 6531  (class class class)co 7405  Basecbs 17228   ↾_s cress 17251  1_rcur 20141  Ringcrg 20193  SubRingcsubrg 20529

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fv 6539  df-ov 7408  df-subrg 20530

This theorem is referenced by:  subrgsubg  20537  subrg1  20542  subrgsubm  20545  subrgdvds  20546  subrguss  20547  subrginv  20548  subrgdv  20549  subrgmre  20557  subsubrg  20558  issubdrg  20740  sdrgss  20753  sdrgacs  20761  subdrgint  20763  abvres  20791  sralmod  21145  cnsubrg  21395  issubassa3  21826  sraassab  21828  sraassa  21829  sraassaOLD  21830  aspid  21835  issubassa2  21852  resspsrbas  21934  resspsradd  21935  resspsrmul  21936  resspsrvsca  21937  mplassa  21982  ressmplbas2  21985  subrgascl  22024  subrgasclcl  22025  mplind  22028  evlsval2  22045  evlssca  22047  evlsscasrng  22055  mpfconst  22059  mpff  22062  mpfaddcl  22063  mpfmulcl  22064  mpfind  22065  ply1assa  22135  evls1val  22258  evls1rhm  22260  evls1sca  22261  evls1scasrng  22277  pf1f  22288  evls1fpws  22307  evls1vsca  22311  asclply1subcl  22312  evls1maplmhm  22315  sranlm  24623  clmsscn  25030  cphreccllem  25130  cphdivcl  25134  cphabscl  25137  cphsqrtcl2  25138  cphsqrtcl3  25139  cphipcl  25143  4cphipval2  25194  resscdrg  25310  srabn  25312  plypf1  26169  dvply2g  26244  dvply2gOLD  26245  taylply2  26327  taylply2OLD  26328  elrgspn  33241  elrgspnsubrunlem1  33242  elrgspnsubrunlem2  33243  elrgspnsubrun  33244  0ringsubrg  33246  subrdom  33279  fldgenssp  33312  idlinsubrg  33446  ressply1evls1  33578  ressasclcl  33584  vr1nz  33603  sralvec  33625  lsssra  33628  drgext0g  33629  drgextvsca  33630  drgext0gsca  33631  drgextsubrg  33632  drgextlsp  33633  drgextgsum  33634  fedgmullem1  33669  fedgmullem2  33670  fedgmul  33671  extdggt0  33699  fldexttr  33700  extdg1id  33707  fldextrspunlsp  33715  fldextrspunlem1  33716  fldextrspunfld  33717  elirng  33727  irngss  33728  0ringirng  33730  ply1annnr  33737  imacrhmcl  42537  evlsval3  42582  evlsvvval  42586  evlsbagval  42589  evlsevl  42594  evlsmhpvvval  42618  mhphf  42620  mhphf2  42621  mhphf3  42622  cnsrexpcl  43189  fsumcnsrcl  43190  cnsrplycl  43191  rgspnid  43192  rngunsnply  43193