Definition df-subrng 13754

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.)

Assertion

Ref	Expression
df-subrng	|- SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )

Distinct variable group:   w, s

Detailed syntax breakdown of Definition df-subrng

Step	Hyp	Ref	Expression
1		csubrng 13753	. 2 class SubRng
2		vw	. . 3 setvar w
3		crng 13488	. . 3 class Rng
4	2	cv 1363	. . . . . 6 class w
5		vs	. . . . . . 7 setvar s
6	5	cv 1363	. . . . . 6 class s
7		cress 12679	. . . . . 6 class ↾s
8	4, 6, 7	co 5922	. . . . 5 class ( w ↾s s )
9	8, 3	wcel 2167	. . . 4 wff ( w ↾s s ) e. Rng
10		cbs 12678	. . . . . 6 class Base
11	4, 10	cfv 5258	. . . . 5 class ( Base ` w )
12	11	cpw 3605	. . . 4 class ~P ( Base ` w )
13	9, 5, 12	crab 2479	. . 3 class { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng }
14	2, 3, 13	cmpt 4094	. 2 class ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
15	1, 14	wceq 1364	1 wff SubRng = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )

This definition is referenced by:  issubrng  13755