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 ⊢ R ↾ A ∈ V → ran ⁡ R ↾ A = ⋃ A / R

Proof

Step Hyp Ref Expression
1 uniqs ⊢ R ↾ A ∈ V → ⋃ A / R = R A
2 df-ima ⊢ R A = ran ⁡ R ↾ A
3 1 2 eqtr2di ⊢ R ↾ A ∈ V → ran ⁡ R ↾ A = ⋃ A / R