This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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