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 dom B B A =


Step Hyp Ref Expression
1 imadisj B A = dom B A =
2 disjsn dom B A = ¬ A dom B
3 1 2 sylbbr ¬ A dom B B A =