Metamath Proof Explorer

Theorem ndmfv

Description: The value of a class outside its domain is the empty set. (An artifact of our function value definition.) (Contributed by NM, 24-Aug-1995)

		Ref	Expression
	Assertion	ndmfv	$⊢ \neg A \in dom F \to F (A) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		euex	$⊢ \exists! x A F x \to \exists x A F x$
2		eldmg	$⊢ A \in V \to (A \in dom F \leftrightarrow \exists x A F x)$
3	1 2	syl5ibr	$⊢ A \in V \to (\exists! x A F x \to A \in dom F)$
4	3	con3d	$⊢ A \in V \to (\neg A \in dom F \to \neg \exists! x A F x)$
5		tz6.12-2	$⊢ \neg \exists! x A F x \to F (A) = \emptyset$
6	4 5	syl6	$⊢ A \in V \to (\neg A \in dom F \to F (A) = \emptyset)$
7		fvprc	$⊢ \neg A \in V \to F (A) = \emptyset$
8	7	a1d	$⊢ \neg A \in V \to (\neg A \in dom F \to F (A) = \emptyset)$
9	6 8	pm2.61i	$⊢ \neg A \in dom F \to F (A) = \emptyset$