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\upharpoonright }_A\in V\to \mathrm{ran}\left({R\upharpoonright }_A\right)=\bigcup \left(A/R\right)$$

Proof

Step	Hyp	Ref	Expression
1		uniqsALTV	$$⊢{R\upharpoonright }_A\in V\to \bigcup \left(A/R\right)=R\left[A\right]$$
2		df-ima	$$⊢R\left[A\right]=\mathrm{ran}\left({R\upharpoonright }_A\right)$$
3	1 2	eqtr2di	$$⊢{R\upharpoonright }_A\in V\to \mathrm{ran}\left({R\upharpoonright }_A\right)=\bigcup \left(A/R\right)$$