MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subrgss Structured version   Unicode version

Theorem subrgss 17543
Description: A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
Hypothesis
Ref Expression
subrgss.1  |-  B  =  ( Base `  R
)
Assertion
Ref Expression
subrgss  |-  ( A  e.  (SubRing `  R
)  ->  A  C_  B
)

Proof of Theorem subrgss
StepHypRef Expression
1 subrgss.1 . . . 4  |-  B  =  ( Base `  R
)
2 eqid 2382 . . . 4  |-  ( 1r
`  R )  =  ( 1r `  R
)
31, 2issubrg 17542 . . 3  |-  ( A  e.  (SubRing `  R
)  <->  ( ( R  e.  Ring  /\  ( Rs  A )  e.  Ring )  /\  ( A  C_  B  /\  ( 1r `  R )  e.  A
) ) )
43simprbi 462 . 2  |-  ( A  e.  (SubRing `  R
)  ->  ( A  C_  B  /\  ( 1r
`  R )  e.  A ) )
54simpld 457 1  |-  ( A  e.  (SubRing `  R
)  ->  A  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399    e. wcel 1826    C_ wss 3389   ` cfv 5496  (class class class)co 6196   Basecbs 14634   ↾s cress 14635   1rcur 17266   Ringcrg 17311  SubRingcsubrg 17538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fv 5504  df-ov 6199  df-subrg 17540
This theorem is referenced by:  subrgsubg  17548  subrg1  17552  subrgsubm  17555  subrgdvds  17556  subrguss  17557  subrginv  17558  subrgdv  17559  subrgmre  17566  issubdrg  17567  subsubrg  17568  abvres  17601  sralmod  17946  issubassa  18086  sraassa  18087  aspid  18092  issubassa2  18107  resspsrbas  18183  resspsradd  18184  resspsrmul  18185  resspsrvsca  18186  mplassa  18229  ressmplbas2  18230  subrgascl  18276  subrgasclcl  18277  mplind  18280  evlsval2  18302  evlssca  18304  evlsscasrng  18308  mpfconst  18312  mpff  18315  mpfaddcl  18316  mpfmulcl  18317  mpfind  18318  ply1assa  18351  evls1val  18470  evls1rhm  18472  evls1sca  18473  evls1scasrng  18488  pf1f  18499  cnsubrg  18591  sranlm  21278  clmsscn  21664  cphreccllem  21710  cphdivcl  21714  cphabscl  21717  cphsqrtcl2  21718  cphsqrtcl3  21719  cphipcl  21723  resscdrg  21883  srabn  21885  plypf1  22694  dvply2g  22766  taylply2  22848  cnsrexpcl  31282  fsumcnsrcl  31283  cnsrplycl  31284  rgspnid  31289  rngunsnply  31290  sdrgacs  31318
  Copyright terms: Public domain W3C validator