Metamath Proof Explorer


Theorem unidmqseq

Description: The union of the domain quotient of a relation is equal to the class A if and only if the range is equal to it as well. (Contributed by Peter Mazsa, 21-Apr-2019) (Revised by Peter Mazsa, 28-Dec-2021)

Ref Expression
Assertion unidmqseq RVRelRdomR/R=AranR=A

Proof

Step Hyp Ref Expression
1 unidmqs RVRelRdomR/R=ranR
2 1 imp RVRelRdomR/R=ranR
3 2 eqeq1d RVRelRdomR/R=AranR=A
4 3 ex RVRelRdomR/R=AranR=A