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 = \{f \in Ring \| {mulGrp}_{f} \in CMnd\}$

Step	Hyp	Ref	Expression
0		ccrg	$class CRing$
1		vf	$setvar f$
2		crg	$class Ring$
3		cmgp	$class mulGrp$
4	1	cv	$setvar f$
5	4 3	cfv	$class {mulGrp}_{f}$
6		ccmn	$class CMnd$
7	5 6	wcel	$wff {mulGrp}_{f} \in CMnd$
8	7 1 2	crab	$class \{f \in Ring \| {mulGrp}_{f} \in CMnd\}$
9	0 8	wceq	$wff CRing = \{f \in Ring \| {mulGrp}_{f} \in CMnd\}$