Definition df-ofld 29129

Description: Define class of all ordered fields. An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.)

Assertion

Ref	Expression
df-ofld	⊢ oField = (Field ∩ oRing)

Detailed syntax breakdown of Definition df-ofld

Step	Hyp	Ref	Expression
1		cofld 29127	. 2 class oField
2		cfield 18571	. . 3 class Field
3		corng 29126	. . 3 class oRing
4	2, 3	cin 3539	. 2 class (Field ∩ oRing)
5	1, 4	wceq 1475	1 wff oField = (Field ∩ oRing)

This definition is referenced by:  isofld  29133