Description: Define the class of domain quotients. Domain quotients are pairs of
sets, typically a relation and a set, where the quotient (see df-qs )
of the relation on its domain is equal to the set. See comments of
df-ers for the motivation for this definition. (Contributed by Peter
Mazsa, 16-Apr-2019)