Metamath Proof Explorer


Syntax definition celdisjs

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

Ref Expression
Assertion celdisjs class ElDisjs