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	⊢ ( ¬ 𝐴 ∈ V → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ )
2	1	fveq1d	⊢ ( ¬ 𝐴 ∈ V → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( ∅ ‘ 𝐵 ) )
3		0fv	⊢ ( ∅ ‘ 𝐵 ) = ∅
4	2 3	eqtrdi	⊢ ( ¬ 𝐴 ∈ V → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ∅ )