Metamath Proof Explorer


Definition df-dmqs

Description: Define the domain quotient predicate. (Read: the domain quotient of R is A .) If A and R are sets, the domain quotient binary relation and the domain quotient predicate are the same, see brdmqssqs . (Contributed by Peter Mazsa, 9-Aug-2021)

Ref Expression
Assertion df-dmqs R DomainQs A dom R / R = A

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 cA class A
2 1 0 wdmqs wff R DomainQs A
3 0 cdm class dom R
4 3 0 cqs class dom R / R
5 4 1 wceq wff dom R / R = A
6 2 5 wb wff R DomainQs A dom R / R = A