This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ran ( 𝑅 ↾ 𝐴 ) = ∪ ( 𝐴 / 𝑅 ) )

Proof

Step Hyp Ref Expression
1 uniqs ⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )
2 df-ima ⊢ ( 𝑅 “ 𝐴 ) = ran ( 𝑅 ↾ 𝐴 )
3 1 2 eqtr2di ⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ran ( 𝑅 ↾ 𝐴 ) = ∪ ( 𝐴 / 𝑅 ) )