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

Metamath Proof Explorer

Definition df-field

Description: Afield is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015)

		Ref	Expression
	Assertion	df-field	$⊢ Field = DivRing \cap CRing$

Step	Hyp	Ref	Expression
0		cfield	$class Field$
1		cdr	$class DivRing$
2		ccrg	$class CRing$
3	1 2	cin	$class (DivRing \cap CRing)$
4	0 3	wceq	$wff Field = DivRing \cap CRing$