Metamath Proof Explorer

Theorem ndmima

Description: The image of a singleton outside the domain is empty. (Contributed by NM, 22-May-1998) (Proof shortened by OpenAI, 3-Jul-2020)

Ref Expression
Assertion ndmima 
|- ( -. A e. dom B -> ( B " { A } ) = (/) )

Proof

Step Hyp Ref Expression
1 imadisj 
 |-  ( ( B " { A } ) = (/) <-> ( dom B i^i { A } ) = (/) )
2 disjsn 
 |-  ( ( dom B i^i { A } ) = (/) <-> -. A e. dom B )
3 1 2 sylbbr 
 |-  ( -. A e. dom B -> ( B " { A } ) = (/) )