fnimadisj

Description: A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007)

		Ref	Expression
	Assertion	fnimadisj	$⊢ (F Fn A \land A \cap C = \emptyset) \to F [C] = \emptyset$

Step	Hyp	Ref	Expression
1		fndm	$⊢ F Fn A \to dom F = A$
2	1	ineq1d	$⊢ F Fn A \to dom F \cap C = A \cap C$
3	2	eqeq1d	$⊢ F Fn A \to (dom F \cap C = \emptyset \leftrightarrow A \cap C = \emptyset)$
4	3	biimpar	$⊢ (F Fn A \land A \cap C = \emptyset) \to dom F \cap C = \emptyset$
5		imadisj	$⊢ F [C] = \emptyset \leftrightarrow dom F \cap C = \emptyset$
6	4 5	sylibr	$⊢ (F Fn A \land A \cap C = \emptyset) \to F [C] = \emptyset$

Metamath Proof Explorer