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

Metamath Proof Explorer

Theorem rnco2

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

		Ref	Expression
	Assertion	rnco2	$⊢ ran (A \circ B) = A [ran B]$

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