Definition df-dmqs 39748

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 39756. (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 39232	. 2 wff 𝑅 DomainQs 𝐴
4	2	cdm 5650	. . . 4 class dom 𝑅
5	4, 2	cqs 8719	. . 3 class (dom 𝑅 / 𝑅)
6	5, 1	wceq 1569	. 2 wff (dom 𝑅 / 𝑅) = 𝐴
7	3, 6	wb 209	1 wff (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)

This definition is used by:  brdmqssqs  39756  cnvepresdmqs  39763  dferALTV2  39778  dfpart2  39897