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	$$⊢\mathrm{DomainQss}=\left\{⟨x,y⟩|\mathrm{dom}x/x=y\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmqss	$$class\mathrm{DomainQss}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4	3	cdm	$$class\mathrm{dom}x$$
5	4 3	cqs	$$class\left(\mathrm{dom}x/x\right)$$
6	2	cv	$$setvary$$
7	5 6	wceq	$$wff\mathrm{dom}x/x=y$$
8	7 1 2	copab	$$class\left\{⟨x,y⟩|\mathrm{dom}x/x=y\right\}$$
9	0 8	wceq	$$wff\mathrm{DomainQss}=\left\{⟨x,y⟩|\mathrm{dom}x/x=y\right\}$$