Theorem subrgss 19519

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ⊆ wss 3924  ‘cfv 6341  (class class class)co 7142  Basecbs 16466   ↾_s cress 16467  1_rcur 19234  Ringcrg 19280  SubRingcsubrg 19514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3488  df-sbc 3764  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fv 6349  df-ov 7145  df-subrg 19516

This theorem is referenced by:  subrgsubg  19524  subrg1  19528  subrgsubm  19531  subrgdvds  19532  subrguss  19533  subrginv  19534  subrgdv  19535  subrgmre  19542  issubdrg  19543  subsubrg  19544  sdrgss  19559  sdrgacs  19563  subdrgint  19565  abvres  19593  sralmod  19942  issubassa3  20080  sraassa  20082  aspid  20087  issubassa2  20104  resspsrbas  20178  resspsradd  20179  resspsrmul  20180  resspsrvsca  20181  mplassa  20218  ressmplbas2  20219  subrgascl  20261  subrgasclcl  20262  mplind  20265  evlsval2  20283  evlssca  20285  evlsscasrng  20293  mpfconst  20297  mpff  20300  mpfaddcl  20301  mpfmulcl  20302  mpfind  20303  ply1assa  20350  evls1val  20466  evls1rhm  20468  evls1sca  20469  evls1scasrng  20485  pf1f  20496  cnsubrg  20588  sranlm  23276  clmsscn  23666  cphreccllem  23765  cphdivcl  23769  cphabscl  23772  cphsqrtcl2  23773  cphsqrtcl3  23774  cphipcl  23778  4cphipval2  23828  resscdrg  23944  srabn  23946  plypf1  24788  dvply2g  24860  taylply2  24942  sralvec  31000  drgext0g  31002  drgextvsca  31003  drgext0gsca  31004  drgextsubrg  31005  drgextlsp  31006  drgextgsum  31007  fedgmullem1  31035  fedgmullem2  31036  fedgmul  31037  extdggt0  31057  fldexttr  31058  extdg1id  31063  selvval2lem4  39211  cnsrexpcl  39857  fsumcnsrcl  39858  cnsrplycl  39859  rgspnid  39864  rngunsnply  39865