![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-cring | Structured version Visualization version GIF version |
Description: Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.) |
Ref | Expression |
---|---|
df-cring | ⊢ CRing = {𝑓 ∈ Ring ∣ (mulGrp‘𝑓) ∈ CMnd} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccrg 19965 | . 2 class CRing | |
2 | vf | . . . . . 6 setvar 𝑓 | |
3 | 2 | cv 1540 | . . . . 5 class 𝑓 |
4 | cmgp 19896 | . . . . 5 class mulGrp | |
5 | 3, 4 | cfv 6496 | . . . 4 class (mulGrp‘𝑓) |
6 | ccmn 19562 | . . . 4 class CMnd | |
7 | 5, 6 | wcel 2106 | . . 3 wff (mulGrp‘𝑓) ∈ CMnd |
8 | crg 19964 | . . 3 class Ring | |
9 | 7, 2, 8 | crab 3407 | . 2 class {𝑓 ∈ Ring ∣ (mulGrp‘𝑓) ∈ CMnd} |
10 | 1, 9 | wceq 1541 | 1 wff CRing = {𝑓 ∈ Ring ∣ (mulGrp‘𝑓) ∈ CMnd} |
Colors of variables: wff setvar class |
This definition is referenced by: iscrng 19971 |
Copyright terms: Public domain | W3C validator |