Definition df-dmqss

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)

	Ref	Expression
Assertion	df-dmqss	|- DomainQss = { <. x , y >. | ( dom x /. x ) = y }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmqss	|- DomainQss
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4	3	cdm	|- dom x
5	4 3	cqs	|- ( dom x /. x )
6	2	cv	|- y
7	5 6	wceq	|- ( dom x /. x ) = y
8	7 1 2	copab	|- { <. x , y >. | ( dom x /. x ) = y }
9	0 8	wceq	|- DomainQss = { <. x , y >. | ( dom x /. x ) = y }