Metamath Proof Explorer


Syntax definition cdif

Description: Extend class notation to include class difference (read: " A minus B ").

Ref Expression
Assertion cdif
class ( A \ B )