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	|- ( -. A e. dom F -> ( F ` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		euex	|- ( E! x A F x -> E. x A F x )
2		eldmg	|- ( A e. _V -> ( A e. dom F <-> E. x A F x ) )
3	1 2	imbitrrid	|- ( A e. _V -> ( E! x A F x -> A e. dom F ) )
4	3	con3d	|- ( A e. _V -> ( -. A e. dom F -> -. E! x A F x ) )
5		tz6.12-2	|- ( -. E! x A F x -> ( F ` A ) = (/) )
6	4 5	syl6	|- ( A e. _V -> ( -. A e. dom F -> ( F ` A ) = (/) ) )
7		fvprc	|- ( -. A e. _V -> ( F ` A ) = (/) )
8	7	a1d	|- ( -. A e. _V -> ( -. A e. dom F -> ( F ` A ) = (/) ) )
9	6 8	pm2.61i	|- ( -. A e. dom F -> ( F ` A ) = (/) )