Definition df-subrng

Description: Define a subring of a non-unital ring as a set of elements that is a non-unital ring in its own right. In this section, a subring of a non-unital ring is simply called "subring", unless it causes any ambiguity with SubRing . (Contributed by AV, 14-Feb-2025)

	Ref	Expression
Assertion	df-subrng	Could not format assertion : No typesetting found for |- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Rng } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubrng	Could not format SubRng : No typesetting found for class SubRng with typecode class
1		vw	$$setvarw$$
2		crng	$$class\mathrm{Rng}$$
3		vs	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_w$$
8		cress	$$class{\upharpoonright }_{𝑠}$$
9	3	cv	$$setvars$$
10	5 9 8	co	$$class\left(w{\upharpoonright }_{𝑠}s\right)$$
11	10 2	wcel	$$wffw{\upharpoonright }_{𝑠}s\in \mathrm{Rng}$$
12	11 3 7	crab	$$class\left\{s\in 𝒫{\mathrm{Base}}_w|w{\upharpoonright }_{𝑠}s\in \mathrm{Rng}\right\}$$
13	1 2 12	cmpt	$$class\left(w\in \mathrm{Rng}⟼\left\{s\in 𝒫{\mathrm{Base}}_w|w{\upharpoonright }_{𝑠}s\in \mathrm{Rng}\right\}\right)$$
14	0 13	wceq	Could not format SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Rng } ) : No typesetting found for wff SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Rng } ) with typecode wff