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