Definition df-dmqs 38657

Description: Define the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.) If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same, see brdmqssqs 38665. (Contributed by Peter Mazsa, 9-Aug-2021.)

Assertion

Ref	Expression
df-dmqs	⊢ (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)

Detailed syntax breakdown of Definition df-dmqs

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wdmqs 38223	. 2 wff 𝑅 DomainQs 𝐴
4	2	cdm 5654	. . . 4 class dom 𝑅
5	4, 2	cqs 8718	. . 3 class (dom 𝑅 / 𝑅)
6	5, 1	wceq 1540	. 2 wff (dom 𝑅 / 𝑅) = 𝐴
7	3, 6	wb 206	1 wff (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)

This definition is referenced by:  brdmqssqs  38665  cnvepresdmqs  38671  dferALTV2  38686  dfpart2  38787