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

Metamath Proof Explorer

Definition df-fld

Description: Definition of a field. A field is a commutative division ring. (Contributed by FL, 6-Sep-2009) (Revised by Jeff Madsen, 10-Jun-2010) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-fld	$⊢ Fld = DivRingOps \cap Com2$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfld	$class Fld$
1		cdrng	$class DivRingOps$
2		ccm2	$class Com2$
3	1 2	cin	$class (DivRingOps \cap Com2)$
4	0 3	wceq	$wff Fld = DivRingOps \cap Com2$