Theorem rnco2

Description: The range of the composition of two classes. (Contributed by NM, 27-Mar-2008)

	Ref	Expression
Assertion	rnco2	$$⊢\mathrm{ran}\left(A\circ B\right)=A\left[\mathrm{ran}B\right]$$

Proof

Step	Hyp	Ref	Expression
1		rnco	$$⊢\mathrm{ran}\left(A\circ B\right)=\mathrm{ran}\left({A\upharpoonright }_{\mathrm{ran}B}\right)$$
2		df-ima	$$⊢A\left[\mathrm{ran}B\right]=\mathrm{ran}\left({A\upharpoonright }_{\mathrm{ran}B}\right)$$
3	1 2	eqtr4i	$$⊢\mathrm{ran}\left(A\circ B\right)=A\left[\mathrm{ran}B\right]$$