Metamath Proof Explorer

Theorem rnfvprc

Description: The range of a function value at a proper class is empty. (Contributed by AV, 20-Aug-2022)

Ref Expression
Hypothesis rnfvprc.y 
|- Y = ( F ` X )
Assertion rnfvprc 
|- ( -. X e. _V -> ran Y = (/) )

Proof

Step Hyp Ref Expression
1 rnfvprc.y 
 |-  Y = ( F ` X )
2 fvprc 
 |-  ( -. X e. _V -> ( F ` X ) = (/) )
3 1 2 eqtrid 
 |-  ( -. X e. _V -> Y = (/) )
4 3 rneqd 
 |-  ( -. X e. _V -> ran Y = ran (/) )
5 rn0 
 |-  ran (/) = (/)
6 4 5 eqtrdi 
 |-  ( -. X e. _V -> ran Y = (/) )