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 |`s A )
Assertion	subsubrg2	|- ( A e. ( SubRing ` R ) -> ( SubRing ` S ) = ( ( SubRing ` R ) i^i ~P A ) )

Proof

Step	Hyp	Ref	Expression
1		subsubrg.s	|- S = ( R |`s A )
2	1	subsubrg	|- ( A e. ( SubRing ` R ) -> ( a e. ( SubRing ` S ) <-> ( a e. ( SubRing ` R ) /\ a C_ A ) ) )
3		elin	|- ( a e. ( ( SubRing ` R ) i^i ~P A ) <-> ( a e. ( SubRing ` R ) /\ a e. ~P A ) )
4		velpw	|- ( a e. ~P A <-> a C_ A )
5	4	anbi2i	|- ( ( a e. ( SubRing ` R ) /\ a e. ~P A ) <-> ( a e. ( SubRing ` R ) /\ a C_ A ) )
6	3 5	bitr2i	|- ( ( a e. ( SubRing ` R ) /\ a C_ A ) <-> a e. ( ( SubRing ` R ) i^i ~P A ) )
7	2 6	bitrdi	|- ( A e. ( SubRing ` R ) -> ( a e. ( SubRing ` S ) <-> a e. ( ( SubRing ` R ) i^i ~P A ) ) )
8	7	eqrdv	|- ( A e. ( SubRing ` R ) -> ( SubRing ` S ) = ( ( SubRing ` R ) i^i ~P A ) )