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 eqtrdi
 |-  ( -. A e. _V -> ( ( F ` A ) ` B ) = (/) )