Metamath Proof Explorer


Syntax definition cdm

Description: Extend the definition of a class to include the domain of a class.

Ref Expression
Assertion cdm class dom 𝐴