Metamath Proof Explorer

Theorem fvprc

Description: A function's value at a proper class is the empty set. (Contributed by NM, 20-May-1998)

Ref Expression
Assertion fvprc 
|- ( -. A e. _V -> ( F ` A ) = (/) )

Proof

Step Hyp Ref Expression
1 brprcneu 
 |-  ( -. A e. _V -> -. E! x A F x )
2 tz6.12-2 
 |-  ( -. E! x A F x -> ( F ` A ) = (/) )
3 1 2 syl 
 |-  ( -. A e. _V -> ( F ` A ) = (/) )