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	|- ( R e. V -> ( Rel R -> ( U. ( dom R /. R ) = A <-> ran R = A ) ) )

Proof

Step	Hyp	Ref	Expression
1		unidmqs	|- ( R e. V -> ( Rel R -> U. ( dom R /. R ) = ran R ) )
2	1	imp	|- ( ( R e. V /\ Rel R ) -> U. ( dom R /. R ) = ran R )
3	2	eqeq1d	|- ( ( R e. V /\ Rel R ) -> ( U. ( dom R /. R ) = A <-> ran R = A ) )
4	3	ex	|- ( R e. V -> ( Rel R -> ( U. ( dom R /. R ) = A <-> ran R = A ) ) )