Definition df-dmqs 35906

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 35914. (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 35509	. 2 wff 𝑅 DomainQs 𝐴
4	2	cdm 5541	. . . 4 class dom 𝑅
5	4, 2	cqs 8274	. . 3 class (dom 𝑅 / 𝑅)
6	5, 1	wceq 1537	. 2 wff (dom 𝑅 / 𝑅) = 𝐴
7	3, 6	wb 208	1 wff (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)

This definition is referenced by:  brdmqssqs  35914  cnvepresdmqs  35919  dferALTV2  35934