Metamath Proof Explorer


Definition df-dmqs

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 𝑅
1 cA 𝐴
2 1 0 wdmqs 𝑅 DomainQs 𝐴
3 0 cdm dom 𝑅
4 3 0 cqs ( dom 𝑅 / 𝑅 )
5 4 1 wceq ( dom 𝑅 / 𝑅 ) = 𝐴
6 2 5 wb ( 𝑅 DomainQs 𝐴 ↔ ( dom 𝑅 / 𝑅 ) = 𝐴 )