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

Proof

Step Hyp Ref Expression
1 cnvcnv2 
 |-  `' `' A = ( A |` _V )
2 1 rneqi 
 |-  ran `' `' A = ran ( A |` _V )
3 rncnvcnv 
 |-  ran `' `' A = ran A
4 2 3 eqtr3i 
 |-  ran ( A |` _V ) = ran A