Metamath Proof Explorer

Theorem rnresequniqs

Description: The range of a restriction is equal to the union of the quotient set. (Contributed by Peter Mazsa, 19-May-2018)

Ref Expression
Assertion rnresequniqs 
|- ( ( R |` A ) e. V -> ran ( R |` A ) = U. ( A /. R ) )

Proof

Step Hyp Ref Expression
1 uniqsALTV 
 |-  ( ( R |` A ) e. V -> U. ( A /. R ) = ( R " A ) )
2 df-ima 
 |-  ( R " A ) = ran ( R |` A )
3 1 2 eqtr2di 
 |-  ( ( R |` A ) e. V -> ran ( R |` A ) = U. ( A /. R ) )