Metamath Proof Explorer


Syntax definition cdisjs

Description: Extend the definition of a class to include the disjoints class, i.e., the disjoint relations class.

Ref Expression
Assertion cdisjs class Disjs