Theorem subrgss 20481

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ⊆ wss 3914  ‘cfv 6511  (class class class)co 7387  Basecbs 17179   ↾_s cress 17200  1_rcur 20090  Ringcrg 20142  SubRingcsubrg 20478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-subrg 20479

This theorem is referenced by:  subrgsubg  20486  subrg1  20491  subrgsubm  20494  subrgdvds  20495  subrguss  20496  subrginv  20497  subrgdv  20498  subrgmre  20506  subsubrg  20507  issubdrg  20689  sdrgss  20702  sdrgacs  20710  subdrgint  20712  abvres  20740  sralmod  21094  cnsubrg  21344  issubassa3  21775  sraassab  21777  sraassa  21778  sraassaOLD  21779  aspid  21784  issubassa2  21801  resspsrbas  21883  resspsradd  21884  resspsrmul  21885  resspsrvsca  21886  mplassa  21931  ressmplbas2  21934  subrgascl  21973  subrgasclcl  21974  mplind  21977  evlsval2  21994  evlssca  21996  evlsscasrng  22004  mpfconst  22008  mpff  22011  mpfaddcl  22012  mpfmulcl  22013  mpfind  22014  ply1assa  22084  evls1val  22207  evls1rhm  22209  evls1sca  22210  evls1scasrng  22226  pf1f  22237  evls1fpws  22256  evls1vsca  22260  asclply1subcl  22261  evls1maplmhm  22264  sranlm  24572  clmsscn  24979  cphreccllem  25078  cphdivcl  25082  cphabscl  25085  cphsqrtcl2  25086  cphsqrtcl3  25087  cphipcl  25091  4cphipval2  25142  resscdrg  25258  srabn  25260  plypf1  26117  dvply2g  26192  dvply2gOLD  26193  taylply2  26275  taylply2OLD  26276  elrgspn  33197  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  elrgspnsubrun  33200  0ringsubrg  33202  subrdom  33235  fldgenssp  33268  idlinsubrg  33402  ressply1evls1  33534  ressasclcl  33540  vr1nz  33559  sralvec  33581  lsssra  33584  drgext0g  33585  drgextvsca  33586  drgext0gsca  33587  drgextsubrg  33588  drgextlsp  33589  drgextgsum  33590  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  extdggt0  33653  fldexttr  33654  extdg1id  33661  fldextrspunlsp  33669  fldextrspunlem1  33670  fldextrspunfld  33671  elirng  33681  irngss  33682  0ringirng  33684  ply1annnr  33693  imacrhmcl  42502  evlsval3  42547  evlsvvval  42551  evlsbagval  42554  evlsevl  42559  evlsmhpvvval  42583  mhphf  42585  mhphf2  42586  mhphf3  42587  cnsrexpcl  43154  fsumcnsrcl  43155  cnsrplycl  43156  rgspnid  43157  rngunsnply  43158