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 V F A B =

Proof

Step Hyp Ref Expression
1 fvprc ¬ A V F A =
2 1 fveq1d ¬ A V F A B = B
3 0fv B =
4 2 3 eqtrdi ¬ A V F A B =