Metamath Proof Explorer

Theorem afv2prc

Description: A function's value at a proper class is not defined, compare with fvprc . (Contributed by AV, 5-Sep-2022)

Ref Expression
Assertion afv2prc 
|- ( -. A e. _V -> ( F '''' A ) e/ ran F )

Proof

Step Hyp Ref Expression
1 prcnel 
 |-  ( -. A e. _V -> -. A e. dom F )
2 ndmafv2nrn 
 |-  ( -. A e. dom F -> ( F '''' A ) e/ ran F )
3 1 2 syl 
 |-  ( -. A e. _V -> ( F '''' A ) e/ ran F )