Syntax Definition cdif 1484

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

Hypotheses

Ref	Expression
cA	class A
cB	class B

Assertion

Ref	Expression
cdif	class (A \ B)

See definition df-dif 1489 for more information.

metamath.org