# Metamath Proof Explorer

## Theorem subrgin

Description: The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014) (Revised by Mario Carneiro, 7-Dec-2014)

Ref Expression
Assertion subrgin ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({R}\right)\right)\to {A}\cap {B}\in \mathrm{SubRing}\left({R}\right)$

### Proof

Step Hyp Ref Expression
1 intprg ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({R}\right)\right)\to \bigcap \left\{{A},{B}\right\}={A}\cap {B}$
2 prssi ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({R}\right)\right)\to \left\{{A},{B}\right\}\subseteq \mathrm{SubRing}\left({R}\right)$
3 prnzg ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left\{{A},{B}\right\}\ne \varnothing$
4 3 adantr ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({R}\right)\right)\to \left\{{A},{B}\right\}\ne \varnothing$
5 subrgint ${⊢}\left(\left\{{A},{B}\right\}\subseteq \mathrm{SubRing}\left({R}\right)\wedge \left\{{A},{B}\right\}\ne \varnothing \right)\to \bigcap \left\{{A},{B}\right\}\in \mathrm{SubRing}\left({R}\right)$
6 2 4 5 syl2anc ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({R}\right)\right)\to \bigcap \left\{{A},{B}\right\}\in \mathrm{SubRing}\left({R}\right)$
7 1 6 eqeltrrd ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {B}\in \mathrm{SubRing}\left({R}\right)\right)\to {A}\cap {B}\in \mathrm{SubRing}\left({R}\right)$