Metamath Proof Explorer


Syntax definition cers

Description: Extend the definition of a class to include the equivalence relations on their domain quotients class.

Ref Expression
Assertion cers class Ers