This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑅 / 𝑅 ) = 𝐴 )