Theorem imadisj

Description: A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007)

	Ref	Expression
Assertion	imadisj	$$⊢A\left[B\right]=\varnothing \leftrightarrow \mathrm{dom}A\cap B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢A\left[B\right]=\mathrm{ran}\left({A\upharpoonright }_B\right)$$
2	1	eqeq1i	$$⊢A\left[B\right]=\varnothing \leftrightarrow \mathrm{ran}\left({A\upharpoonright }_B\right)=\varnothing$$
3		dm0rn0	$$⊢\mathrm{dom}\left({A\upharpoonright }_B\right)=\varnothing \leftrightarrow \mathrm{ran}\left({A\upharpoonright }_B\right)=\varnothing$$
4		dmres	$$⊢\mathrm{dom}\left({A\upharpoonright }_B\right)=B\cap \mathrm{dom}A$$
5		incom	$$⊢B\cap \mathrm{dom}A=\mathrm{dom}A\cap B$$
6	4 5	eqtri	$$⊢\mathrm{dom}\left({A\upharpoonright }_B\right)=\mathrm{dom}A\cap B$$
7	6	eqeq1i	$$⊢\mathrm{dom}\left({A\upharpoonright }_B\right)=\varnothing \leftrightarrow \mathrm{dom}A\cap B=\varnothing$$
8	2 3 7	3bitr2i	$$⊢A\left[B\right]=\varnothing \leftrightarrow \mathrm{dom}A\cap B=\varnothing$$