Theorem brdmqss

Description: The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019)

	Ref	Expression
Assertion	brdmqss	$$⊢\left(A\in V\wedge R\in W\right)\to \left(R\mathrm{DomainQss}A\leftrightarrow \mathrm{dom}R/R=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dmqseq	$$⊢x=R\to \mathrm{dom}x/x=\mathrm{dom}R/R$$
2		id	$$⊢y=A\to y=A$$
3	1 2	eqeqan12d	$$⊢\left(x=R\wedge y=A\right)\to \left(\mathrm{dom}x/x=y\leftrightarrow \mathrm{dom}R/R=A\right)$$
4		df-dmqss	$$⊢\mathrm{DomainQss}=\left\{⟨x,y⟩|\mathrm{dom}x/x=y\right\}$$
5	3 4	brabga	$$⊢\left(R\in W\wedge A\in V\right)\to \left(R\mathrm{DomainQss}A\leftrightarrow \mathrm{dom}R/R=A\right)$$
6	5	ancoms	$$⊢\left(A\in V\wedge R\in W\right)\to \left(R\mathrm{DomainQss}A\leftrightarrow \mathrm{dom}R/R=A\right)$$