Metamath Proof Explorer

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 ∈ Rng ⟼ s ∈ 𝒫 Base w | w ↾ 𝑠 s ∈ Rng

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubrng class SubRng
1 vw setvar w
2 crng class Rng
3 vs setvar s
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 Base w
8 cress class ↾ 𝑠
9 3 cv setvar s
10 5 9 8 co class w ↾ 𝑠 s
11 10 2 wcel wff w ↾ 𝑠 s ∈ Rng
12 11 3 7 crab class s ∈ 𝒫 Base w | w ↾ 𝑠 s ∈ Rng
13 1 2 12 cmpt class w ∈ Rng ⟼ s ∈ 𝒫 Base w | w ↾ 𝑠 s ∈ Rng
14 0 13 wceq wff SubRng = w ∈ Rng ⟼ s ∈ 𝒫 Base w | w ↾ 𝑠 s ∈ Rng