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 = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rnfvprc.y | |- Y = ( F ` X ) |
|
| 2 | fvprc | |- ( -. X e. _V -> ( F ` X ) = (/) ) |
|
| 3 | 1 2 | syl5eq | |- ( -. 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 = (/) ) |