Definition df-subrng 20485

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 = (𝑤 ∈ Rng ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Rng})

Distinct variable group:   𝑤,𝑠

Detailed syntax breakdown of Definition df-subrng

Step	Hyp	Ref	Expression
1		csubrng 20484	. 2 class SubRng
2		vw	. . 3 setvar 𝑤
3		crng 20094	. . 3 class Rng
4	2	cv 1532	. . . . . 6 class 𝑤
5		vs	. . . . . . 7 setvar 𝑠
6	5	cv 1532	. . . . . 6 class 𝑠
7		cress 17206	. . . . . 6 class ↾s
8	4, 6, 7	co 7414	. . . . 5 class (𝑤 ↾s 𝑠)
9	8, 3	wcel 2098	. . . 4 wff (𝑤 ↾s 𝑠) ∈ Rng
10		cbs 17177	. . . . . 6 class Base
11	4, 10	cfv 6541	. . . . 5 class (Base‘𝑤)
12	11	cpw 4596	. . . 4 class 𝒫 (Base‘𝑤)
13	9, 5, 12	crab 3419	. . 3 class {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Rng}
14	2, 3, 13	cmpt 5224	. 2 class (𝑤 ∈ Rng ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Rng})
15	1, 14	wceq 1533	1 wff SubRng = (𝑤 ∈ Rng ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Rng})

This definition is referenced by:  issubrng  20486