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

Proof

Step	Hyp	Ref	Expression
1		euex	⊢ ( ∃! 𝑥 𝐴 𝐹 𝑥 → ∃ 𝑥 𝐴 𝐹 𝑥 )
2		eldmg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ dom 𝐹 ↔ ∃ 𝑥 𝐴 𝐹 𝑥 ) )
3	1 2	syl5ibr	⊢ ( 𝐴 ∈ V → ( ∃! 𝑥 𝐴 𝐹 𝑥 → 𝐴 ∈ dom 𝐹 ) )
4	3	con3d	⊢ ( 𝐴 ∈ V → ( ¬ 𝐴 ∈ dom 𝐹 → ¬ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
5		tz6.12-2	⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ‘ 𝐴 ) = ∅ )
6	4 5	syl6	⊢ ( 𝐴 ∈ V → ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
7		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ )
8	7	a1d	⊢ ( ¬ 𝐴 ∈ V → ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
9	6 8	pm2.61i	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )