Theorem subsubrng2

Description: The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025)

	Ref	Expression
Hypothesis	subsubrng.s	|- S = ( R |`s A )
Assertion	subsubrng2	|- ( A e. ( SubRng ` R ) -> ( SubRng ` S ) = ( ( SubRng ` R ) i^i ~P A ) )

Proof

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