Theorem rnresv

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

	Ref	Expression
Assertion	rnresv	⊢ ran ( 𝐴 ↾ V ) = ran 𝐴

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	⊢ ◡ ◡ 𝐴 = ( 𝐴 ↾ V )
2	1	rneqi	⊢ ran ◡ ◡ 𝐴 = ran ( 𝐴 ↾ V )
3		rncnvcnv	⊢ ran ◡ ◡ 𝐴 = ran 𝐴
4	2 3	eqtr3i	⊢ ran ( 𝐴 ↾ V ) = ran 𝐴