Theorem subrgss 20854

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900  ‘cfv 6558  (class class class)co 7443  Basecbs 17416   ↾_s cress 17437  1_rcur 20437  Ringcrg 20489  SubRingcsubrg 20851

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fv 6566  df-ov 7446  df-subrg 20852

This theorem is used by:  subrgsubg  20859  subrg1  20864  subrgsubm  20867  subrgdvds  20868  subrguss  20869  subrginv  20870  subrgdv  20871  subrgmre  20879  subsubrg  20880  issubdrg  21067  sdrgss  21080  sdrgacs  21088  subdrgint  21090  abvres  21118  sralmod  21492  cnsubrg  21763  issubassa3  22204  sraassab  22206  sraassa  22207  aspid  22212  issubassa2  22230  resspsrbas  22311  resspsradd  22312  resspsrmul  22313  resspsrvsca  22314  mplassa  22359  ressmplbas2  22365  subrgascl  22405  subrgasclcl  22406  mplind  22409  evlsval2  22426  evlsval3  22428  evlsvvval  22432  evlssca  22433  evlsscasrng  22444  mpfconst  22448  mpff  22451  mpfaddcl  22452  mpfmulcl  22453  mpfind  22454  evlsevl  22471  ply1assa  22547  evls1val  22668  evls1rhm  22670  evls1sca  22671  evls1scasrng  22687  pf1f  22698  evls1fpws  22717  evls1vsca  22721  asclply1subcl  22722  evls1maplmhm  22725  sranlm  25033  clmsscn  25430  cphreccllem  25529  cphdivcl  25533  cphabscl  25536  cphsqrtcl2  25537  cphsqrtcl3  25538  cphipcl  25542  4cphipval2  25593  resscdrg  25709  srabn  25711  plypf1  26561  dvply2g  26636  taylply2  26725  elrgspn  33877  elrgspnsubrunlem1  33878  elrgspnsubrunlem2  33879  elrgspnsubrun  33880  0ringsubrg  33882  subrdom  33916  fldgenssp  33950  idlinsubrg  34051  ressply1evls1  34167  ressasclcl  34173  vr1nz  34195  sralvec  34287  lsssra  34290  drgext0g  34292  drgextvsca  34293  drgext0gsca  34294  drgextsubrg  34295  drgextlsp  34296  drgextgsum  34297  fedgmullem1  34331  fedgmullem2  34332  fedgmul  34333  extdggt0  34359  fldexttr  34360  extdg1id  34368  fldextrspunlsp  34376  fldextrspunlem1  34377  fldextrspunfld  34378  elirng  34388  irngss  34389  0ringirng  34391  ply1annnr  34405  imacrhmcl  43774  evlsbagval  43807  evlsmhpvvval  43816  mhphf  43818  mhphf2  43819  mhphf3  43820  cnsrexpcl  44359  fsumcnsrcl  44360  cnsrplycl  44361  rgspnid  44362  rngunsnply  44363