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	$$⊢\neg A\in \mathrm{dom}B\to B\left[\left\{A\right\}\right]=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		imadisj	$$⊢B\left[\left\{A\right\}\right]=\varnothing \leftrightarrow \mathrm{dom}B\cap \left\{A\right\}=\varnothing$$
2		disjsn	$$⊢\mathrm{dom}B\cap \left\{A\right\}=\varnothing \leftrightarrow \neg A\in \mathrm{dom}B$$
3	1 2	sylbbr	$$⊢\neg A\in \mathrm{dom}B\to B\left[\left\{A\right\}\right]=\varnothing$$