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 [B] = \emptyset \leftrightarrow dom A \cap B = \emptyset$

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

Metamath Proof Explorer