Theorem subrgss 20785

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 2760	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
3	1, 2	issubrg 20784	. . 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 2145   ⊆ wss 3898  ‘cfv 6527  (class class class)co 7408  Basecbs 17348   ↾_s cress 17369  1_rcur 20368  Ringcrg 20420  SubRingcsubrg 20782

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fv 6535  df-ov 7411  df-subrg 20783

This theorem is used by:  subrgsubg  20790  subrg1  20795  subrgsubm  20798  subrgdvds  20799  subrguss  20800  subrginv  20801  subrgdv  20802  subrgmre  20810  subsubrg  20811  issubdrg  20998  sdrgss  21011  sdrgacs  21019  subdrgint  21021  abvres  21049  sralmod  21423  cnsubrg  21694  issubassa3  22135  sraassab  22137  sraassa  22138  aspid  22143  issubassa2  22161  resspsrbas  22242  resspsradd  22243  resspsrmul  22244  resspsrvsca  22245  mplassa  22290  ressmplbas2  22296  subrgascl  22336  subrgasclcl  22337  mplind  22340  evlsval2  22357  evlsval3  22359  evlsvvval  22363  evlssca  22364  evlsscasrng  22375  mpfconst  22379  mpff  22382  mpfaddcl  22383  mpfmulcl  22384  mpfind  22385  evlsevl  22402  ply1assa  22478  evls1val  22599  evls1rhm  22601  evls1sca  22602  evls1scasrng  22618  pf1f  22629  evls1fpws  22648  evls1vsca  22652  asclply1subcl  22653  evls1maplmhm  22656  sranlm  24964  clmsscn  25361  cphreccllem  25460  cphdivcl  25464  cphabscl  25467  cphsqrtcl2  25468  cphsqrtcl3  25469  cphipcl  25473  4cphipval2  25524  resscdrg  25640  srabn  25642  plypf1  26492  dvply2g  26569  taylply2  26658  elrgspn  33740  elrgspnsubrunlem1  33741  elrgspnsubrunlem2  33742  elrgspnsubrun  33743  0ringsubrg  33745  subrdom  33779  fldgenssp  33813  idlinsubrg  33914  ressply1evls1  34030  ressasclcl  34036  vr1nz  34058  sralvec  34150  lsssra  34153  drgext0g  34155  drgextvsca  34156  drgext0gsca  34157  drgextsubrg  34158  drgextlsp  34159  drgextgsum  34160  fedgmullem1  34194  fedgmullem2  34195  fedgmul  34196  extdggt0  34222  fldexttr  34223  extdg1id  34231  fldextrspunlsp  34239  fldextrspunlem1  34240  fldextrspunfld  34241  elirng  34251  irngss  34252  0ringirng  34254  ply1annnr  34268  imacrhmcl  43506  evlsbagval  43536  evlsmhpvvval  43545  mhphf  43547  mhphf2  43548  mhphf3  43549  cnsrexpcl  44110  fsumcnsrcl  44111  cnsrplycl  44112  rgspnid  44113  rngunsnply  44114