Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > subrgss | Structured version Visualization version GIF version |
Description: A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
Ref | Expression |
---|---|
subrgss.1 | ⊢ 𝐵 = (Base‘𝑅) |
Ref | Expression |
---|---|
subrgss | ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subrgss.1 | . . . 4 ⊢ 𝐵 = (Base‘𝑅) | |
2 | eqid 2610 | . . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅) | |
3 | 1, 2 | issubrg 18603 | . . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴))) |
4 | 3 | simprbi 479 | . 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐴 ⊆ 𝐵 ∧ (1r‘𝑅) ∈ 𝐴)) |
5 | 4 | simpld 474 | 1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ⊆ wss 3540 ‘cfv 5804 (class class class)co 6549 Basecbs 15695 ↾s cress 15696 1rcur 18324 Ringcrg 18370 SubRingcsubrg 18599 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fv 5812 df-ov 6552 df-subrg 18601 |
This theorem is referenced by: subrgsubg 18609 subrg1 18613 subrgsubm 18616 subrgdvds 18617 subrguss 18618 subrginv 18619 subrgdv 18620 subrgmre 18627 issubdrg 18628 subsubrg 18629 abvres 18662 sralmod 19008 issubassa 19145 sraassa 19146 aspid 19151 issubassa2 19166 resspsrbas 19236 resspsradd 19237 resspsrmul 19238 resspsrvsca 19239 mplassa 19275 ressmplbas2 19276 subrgascl 19319 subrgasclcl 19320 mplind 19323 evlsval2 19341 evlssca 19343 evlsscasrng 19347 mpfconst 19351 mpff 19354 mpfaddcl 19355 mpfmulcl 19356 mpfind 19357 ply1assa 19390 evls1val 19506 evls1rhm 19508 evls1sca 19509 evls1scasrng 19524 pf1f 19535 cnsubrg 19625 sranlm 22298 clmsscn 22687 cphreccllem 22786 cphdivcl 22790 cphabscl 22793 cphsqrtcl2 22794 cphsqrtcl3 22795 cphipcl 22799 4cphipval2 22849 resscdrg 22962 srabn 22964 plypf1 23772 dvply2g 23844 taylply2 23926 cnsrexpcl 36754 fsumcnsrcl 36755 cnsrplycl 36756 rgspnid 36761 rngunsnply 36762 sdrgacs 36790 |
Copyright terms: Public domain | W3C validator |