Metamath Proof Explorer

Theorem fv2prc

Description: A function value of a function value at a proper class is the empty set. (Contributed by AV, 8-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 fvprc 
 |-  ( -. A e. _V -> ( F ` A ) = (/) )
2 1 fveq1d 
 |-  ( -. A e. _V -> ( ( F ` A ) ` B ) = ( (/) ` B ) )
3 0fv 
 |-  ( (/) ` B ) = (/)
4 2 3 syl6eq 
 |-  ( -. A e. _V -> ( ( F ` A ) ` B ) = (/) )