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

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 
|- ( -. 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 ) = (/) )