Theorem dmqseqim

Description: If the domain quotient of a relation is equal to the class A , then the range of the relation is the union of the class. (Contributed by Peter Mazsa, 29-Dec-2021)

	Ref	Expression
Assertion	dmqseqim	|- ( R e. V -> ( Rel R -> ( ( dom R /. R ) = A -> ran R = U. A ) ) )

Proof

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