This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \neg A \in V \to F (A) (B) = \emptyset$

Step	Hyp	Ref	Expression
1		fvprc	$⊢ \neg A \in V \to F (A) = \emptyset$
2	1	fveq1d	$⊢ \neg A \in V \to F (A) (B) = \emptyset (B)$
3		0fv	$⊢ \emptyset (B) = \emptyset$
4	2 3	eqtrdi	$⊢ \neg A \in V \to F (A) (B) = \emptyset$