Theorem subrgss 19655

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1542   ∈ wcel 2114   ⊆ wss 3843  ‘cfv 6339  (class class class)co 7170  Basecbs 16586   ↾_s cress 16587  1_rcur 19370  Ringcrg 19416  SubRingcsubrg 19650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fv 6347  df-ov 7173  df-subrg 19652

This theorem is referenced by:  subrgsubg  19660  subrg1  19664  subrgsubm  19667  subrgdvds  19668  subrguss  19669  subrginv  19670  subrgdv  19671  subrgmre  19678  issubdrg  19679  subsubrg  19680  sdrgss  19695  sdrgacs  19699  subdrgint  19701  abvres  19729  sralmod  20078  cnsubrg  20277  issubassa3  20681  sraassa  20683  aspid  20688  issubassa2  20706  resspsrbas  20794  resspsradd  20795  resspsrmul  20796  resspsrvsca  20797  mplassa  20837  ressmplbas2  20838  subrgascl  20878  subrgasclcl  20879  mplind  20882  evlsval2  20901  evlssca  20903  evlsscasrng  20911  mpfconst  20915  mpff  20918  mpfaddcl  20919  mpfmulcl  20920  mpfind  20921  ply1assa  20974  evls1val  21090  evls1rhm  21092  evls1sca  21093  evls1scasrng  21109  pf1f  21120  sranlm  23437  clmsscn  23831  cphreccllem  23930  cphdivcl  23934  cphabscl  23937  cphsqrtcl2  23938  cphsqrtcl3  23939  cphipcl  23943  4cphipval2  23994  resscdrg  24110  srabn  24112  plypf1  24961  dvply2g  25033  taylply2  25115  idlinsubrg  31180  sralvec  31247  drgext0g  31249  drgextvsca  31250  drgext0gsca  31251  drgextsubrg  31252  drgextlsp  31253  drgextgsum  31254  fedgmullem1  31282  fedgmullem2  31283  fedgmul  31284  extdggt0  31304  fldexttr  31305  extdg1id  31310  selvval2lem4  39810  evlsval3  39851  evlsbagval  39854  mhphf  39864  cnsrexpcl  40562  fsumcnsrcl  40563  cnsrplycl  40564  rgspnid  40569  rngunsnply  40570