Definition df-dmqss 38639

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 8751) of the relation on its domain is equal to the set. See comments of df-ers 38664 for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019.)

Assertion

Ref	Expression
df-dmqss	⊢ DomainQss = {⟨𝑥, 𝑦⟩ ∣ (dom 𝑥 / 𝑥) = 𝑦}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-dmqss

Step	Hyp	Ref	Expression
1		cdmqss 38205	. 2 class DomainQss
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1539	. . . . . 6 class 𝑥
4	3	cdm 5685	. . . . 5 class dom 𝑥
5	4, 3	cqs 8744	. . . 4 class (dom 𝑥 / 𝑥)
6		vy	. . . . 5 setvar 𝑦
7	6	cv 1539	. . . 4 class 𝑦
8	5, 7	wceq 1540	. . 3 wff (dom 𝑥 / 𝑥) = 𝑦
9	8, 2, 6	copab 5205	. 2 class {⟨𝑥, 𝑦⟩ ∣ (dom 𝑥 / 𝑥) = 𝑦}
10	1, 9	wceq 1540	1 wff DomainQss = {⟨𝑥, 𝑦⟩ ∣ (dom 𝑥 / 𝑥) = 𝑦}

This definition is referenced by:  brdmqss  38647