# Metamath Proof Explorer

## Theorem subsubrg2

Description: The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Hypothesis subsubrg.s ${⊢}{S}={R}{↾}_{𝑠}{A}$
Assertion subsubrg2 ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \mathrm{SubRing}\left({S}\right)=\mathrm{SubRing}\left({R}\right)\cap 𝒫{A}$

### Proof

Step Hyp Ref Expression
1 subsubrg.s ${⊢}{S}={R}{↾}_{𝑠}{A}$
2 1 subsubrg ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left({a}\in \mathrm{SubRing}\left({S}\right)↔\left({a}\in \mathrm{SubRing}\left({R}\right)\wedge {a}\subseteq {A}\right)\right)$
3 elin ${⊢}{a}\in \left(\mathrm{SubRing}\left({R}\right)\cap 𝒫{A}\right)↔\left({a}\in \mathrm{SubRing}\left({R}\right)\wedge {a}\in 𝒫{A}\right)$
4 velpw ${⊢}{a}\in 𝒫{A}↔{a}\subseteq {A}$
5 4 anbi2i ${⊢}\left({a}\in \mathrm{SubRing}\left({R}\right)\wedge {a}\in 𝒫{A}\right)↔\left({a}\in \mathrm{SubRing}\left({R}\right)\wedge {a}\subseteq {A}\right)$
6 3 5 bitr2i ${⊢}\left({a}\in \mathrm{SubRing}\left({R}\right)\wedge {a}\subseteq {A}\right)↔{a}\in \left(\mathrm{SubRing}\left({R}\right)\cap 𝒫{A}\right)$
7 2 6 syl6bb ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left({a}\in \mathrm{SubRing}\left({S}\right)↔{a}\in \left(\mathrm{SubRing}\left({R}\right)\cap 𝒫{A}\right)\right)$
8 7 eqrdv ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \mathrm{SubRing}\left({S}\right)=\mathrm{SubRing}\left({R}\right)\cap 𝒫{A}$