Metamath Proof Explorer

Theorem 0fv

Description: Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014)

Ref Expression
Assertion 0fv 
|- ( (/) ` A ) = (/)

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. A e. (/)
2 dm0 
 |-  dom (/) = (/)
3 2 eleq2i 
 |-  ( A e. dom (/) <-> A e. (/) )
4 1 3 mtbir 
 |-  -. A e. dom (/)
5 ndmfv 
 |-  ( -. A e. dom (/) -> ( (/) ` A ) = (/) )
6 4 5 ax-mp 
 |-  ( (/) ` A ) = (/)