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 ∩ Com2 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfld	⊢ Fld
1		cdrng	⊢ DivRingOps
2		ccm2	⊢ Com2
3	1 2	cin	⊢ ( DivRingOps ∩ Com2 )
4	0 3	wceq	⊢ Fld = ( DivRingOps ∩ Com2 )