Metamath Proof Explorer


Syntax definition cufl

Description: Extend class notation with the ultrafilter lemma.

Ref Expression
Assertion cufl class UFL