Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dmqs Structured version   Visualization version   GIF version

Definition df-dmqs 36731
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 36739. (Contributed by Peter Mazsa, 9-Aug-2021.)
Assertion
Ref Expression
df-dmqs (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)

Detailed syntax breakdown of Definition df-dmqs
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wdmqs 36336 . 2 wff 𝑅 DomainQs 𝐴
42cdm 5588 . . . 4 class dom 𝑅
54, 2cqs 8471 . . 3 class (dom 𝑅 / 𝑅)
65, 1wceq 1541 . 2 wff (dom 𝑅 / 𝑅) = 𝐴
73, 6wb 205 1 wff (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  brdmqssqs  36739  cnvepresdmqs  36744  dferALTV2  36759
  Copyright terms: Public domain W3C validator