MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-subrng Structured version   Visualization version   GIF version

Definition df-subrng 20446
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
StepHypRef Expression
1 csubrng 20445 . 2 class SubRng
2 vw . . 3 setvar 𝑤
3 crng 20057 . . 3 class Rng
42cv 1532 . . . . . 6 class 𝑤
5 vs . . . . . . 7 setvar 𝑠
65cv 1532 . . . . . 6 class 𝑠
7 cress 17182 . . . . . 6 class s
84, 6, 7co 7405 . . . . 5 class (𝑤s 𝑠)
98, 3wcel 2098 . . . 4 wff (𝑤s 𝑠) ∈ Rng
10 cbs 17153 . . . . . 6 class Base
114, 10cfv 6537 . . . . 5 class (Base‘𝑤)
1211cpw 4597 . . . 4 class 𝒫 (Base‘𝑤)
139, 5, 12crab 3426 . . 3 class {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤s 𝑠) ∈ Rng}
142, 3, 13cmpt 5224 . 2 class (𝑤 ∈ Rng ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤s 𝑠) ∈ Rng})
151, 14wceq 1533 1 wff SubRng = (𝑤 ∈ Rng ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤s 𝑠) ∈ Rng})
Colors of variables: wff setvar class
This definition is referenced by:  issubrng  20447
  Copyright terms: Public domain W3C validator