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{\upharpoonright }_{𝑠}A$$
Assertion	subsubrng2	Could not format assertion : No typesetting found for |- ( A e. ( SubRng ` R ) -> ( SubRng ` S ) = ( ( SubRng ` R ) i^i ~P A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		subsubrng.s	$$⊢S=R{\upharpoonright }_{𝑠}A$$
2	1	subsubrng	Could not format ( A e. ( SubRng ` R ) -> ( a e. ( SubRng ` S ) <-> ( a e. ( SubRng ` R ) /\ a C_ A ) ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> ( a e. ( SubRng ` S ) <-> ( a e. ( SubRng ` R ) /\ a C_ A ) ) ) with typecode |-
3		elin	Could not format ( a e. ( ( SubRng ` R ) i^i ~P A ) <-> ( a e. ( SubRng ` R ) /\ a e. ~P A ) ) : No typesetting found for |- ( a e. ( ( SubRng ` R ) i^i ~P A ) <-> ( a e. ( SubRng ` R ) /\ a e. ~P A ) ) with typecode |-
4		velpw	$$⊢a\in 𝒫A\leftrightarrow a\subseteq A$$
5	4	anbi2i	Could not format ( ( a e. ( SubRng ` R ) /\ a e. ~P A ) <-> ( a e. ( SubRng ` R ) /\ a C_ A ) ) : No typesetting found for |- ( ( a e. ( SubRng ` R ) /\ a e. ~P A ) <-> ( a e. ( SubRng ` R ) /\ a C_ A ) ) with typecode |-
6	3 5	bitr2i	Could not format ( ( a e. ( SubRng ` R ) /\ a C_ A ) <-> a e. ( ( SubRng ` R ) i^i ~P A ) ) : No typesetting found for |- ( ( a e. ( SubRng ` R ) /\ a C_ A ) <-> a e. ( ( SubRng ` R ) i^i ~P A ) ) with typecode |-
7	2 6	bitrdi	Could not format ( A e. ( SubRng ` R ) -> ( a e. ( SubRng ` S ) <-> a e. ( ( SubRng ` R ) i^i ~P A ) ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> ( a e. ( SubRng ` S ) <-> a e. ( ( SubRng ` R ) i^i ~P A ) ) ) with typecode |-
8	7	eqrdv	Could not format ( A e. ( SubRng ` R ) -> ( SubRng ` S ) = ( ( SubRng ` R ) i^i ~P A ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> ( SubRng ` S ) = ( ( SubRng ` R ) i^i ~P A ) ) with typecode |-