Metamath Proof Explorer


Syntax definition wdmqs

Description: Extend the definition of a wff to include the domain quotient predicate. (Read: the domain quotient of R is A .)

Ref Expression
Assertion wdmqs wff R DomainQs A