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

Metamath Proof Explorer

Theorem rnresv

Description: The range of a universal restriction. (Contributed by NM, 14-May-2008)

		Ref	Expression
	Assertion	rnresv	$⊢ ran ({A ↾}_{V}) = ran A$

Step	Hyp	Ref	Expression
1		cnvcnv2	$⊢ {A^{-1}}^{-1} = {A ↾}_{V}$
2	1	rneqi	$⊢ ran {A^{-1}}^{-1} = ran ({A ↾}_{V})$
3		rncnvcnv	$⊢ ran {A^{-1}}^{-1} = ran A$
4	2 3	eqtr3i	$⊢ ran ({A ↾}_{V}) = ran A$