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	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Rng } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubrng	|- SubRng
1		vw	|- w
2		crng	|- Rng
3		vs	|- s
4		cbs	|- Base
5	1	cv	|- w
6	5 4	cfv	|- ( Base ` w )
7	6	cpw	|- ~P ( Base ` w )
8		cress	|- |`s
9	3	cv	|- s
10	5 9 8	co	|- ( w |`s s )
11	10 2	wcel	|- ( w |`s s ) e. Rng
12	11 3 7	crab	|- { s e. ~P ( Base ` w ) | ( w |`s s ) e. Rng }
13	1 2 12	cmpt	|- ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Rng } )
14	0 13	wceq	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w |`s s ) e. Rng } )