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	$$⊢\neg A\in \mathrm{V}\to F\left(A\right)\left(B\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fvprc	$$⊢\neg A\in \mathrm{V}\to F\left(A\right)=\varnothing$$
2	1	fveq1d	$$⊢\neg A\in \mathrm{V}\to F\left(A\right)\left(B\right)=\varnothing \left(B\right)$$
3		0fv	$$⊢\varnothing \left(B\right)=\varnothing$$
4	2 3	syl6eq	$$⊢\neg A\in \mathrm{V}\to F\left(A\right)\left(B\right)=\varnothing$$