Metamath Proof Explorer


Syntax definition cdif

Description: Syntax for the difference of two classes.

Ref Expression
Assertion cdif class ( 𝐴 ∖ 𝐵 )