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 SubRing R SubRing S = SubRing R 𝒫 A

Proof

Step Hyp Ref Expression
1 subsubrg.s S = R 𝑠 A
2 1 subsubrg A SubRing R a SubRing S a SubRing R a A
3 elin a SubRing R 𝒫 A a SubRing R a 𝒫 A
4 velpw a 𝒫 A a A
5 4 anbi2i a SubRing R a 𝒫 A a SubRing R a A
6 3 5 bitr2i a SubRing R a A a SubRing R 𝒫 A
7 2 6 bitrdi A SubRing R a SubRing S a SubRing R 𝒫 A
8 7 eqrdv A SubRing R SubRing S = SubRing R 𝒫 A