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

Metamath Proof Explorer

Definition df-cring

Description: Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Assertion df-cring CRing = { 𝑓 ∈ Ring ∣ ( mulGrp ‘ 𝑓 ) ∈ CMnd }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccrg ⊢ CRing
1 vf ⊢ 𝑓
2 crg ⊢ Ring
3 cmgp ⊢ mulGrp
4 1 cv ⊢ 𝑓
5 4 3 cfv ⊢ ( mulGrp ‘ 𝑓 )
6 ccmn ⊢ CMnd
7 5 6 wcel ⊢ ( mulGrp ‘ 𝑓 ) ∈ CMnd
8 7 1 2 crab ⊢ { 𝑓 ∈ Ring ∣ ( mulGrp ‘ 𝑓 ) ∈ CMnd }
9 0 8 wceq ⊢ CRing = { 𝑓 ∈ Ring ∣ ( mulGrp ‘ 𝑓 ) ∈ CMnd }