Metamath Proof Explorer


Syntax definition cfld

Description: Extend class notation with the class of all fields.

Ref Expression
Assertion cfld class Fld