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

Metamath Proof Explorer

Theorem brdmqssqs

Description: If A and R are sets, the domain quotient binary relation and the domain quotient predicate are the same. (Contributed by Peter Mazsa, 14-Aug-2021)

		Ref	Expression
	Assertion	brdmqssqs	$⊢ (A \in V \land R \in W) \to (R DomainQss A \leftrightarrow R DomainQs A)$

Proof

Step	Hyp	Ref	Expression
1		brdmqss	$⊢ (A \in V \land R \in W) \to (R DomainQss A \leftrightarrow dom R / R = A)$
2		df-dmqs	$⊢ R DomainQs A \leftrightarrow dom R / R = A$
3	1 2	bitr4di	$⊢ (A \in V \land R \in W) \to (R DomainQss A \leftrightarrow R DomainQs A)$