Definition df-dmqs 38640

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 38648. (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 38206	. 2 wff 𝑅 DomainQs 𝐴
4	2	cdm 5685	. . . 4 class dom 𝑅
5	4, 2	cqs 8744	. . 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  38648  cnvepresdmqs  38654  dferALTV2  38669  dfpart2  38770