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	$$⊢RDomainQsA\leftrightarrow \mathrm{dom}R/R=A$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	wdmqs	$$wffRDomainQsA$$
3	0	cdm	$$class\mathrm{dom}R$$
4	3 0	cqs	$$class\left(\mathrm{dom}R/R\right)$$
5	4 1	wceq	$$wff\mathrm{dom}R/R=A$$
6	2 5	wb	$$wff\left(RDomainQsA\leftrightarrow \mathrm{dom}R/R=A\right)$$