Metamath Proof Explorer

Theorem fnimaeq0

Description: Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 . (Contributed by Stefan O'Rear, 21-Jan-2015)

		Ref	Expression
	Assertion	fnimaeq0	$⊢ (F Fn A \land B \subseteq A) \to (F [B] = \emptyset \leftrightarrow B = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		imadisj	$⊢ F [B] = \emptyset \leftrightarrow dom F \cap B = \emptyset$
2		incom	$⊢ dom F \cap B = B \cap dom F$
3		fndm	$⊢ F Fn A \to dom F = A$
4	3	sseq2d	$⊢ F Fn A \to (B \subseteq dom F \leftrightarrow B \subseteq A)$
5	4	biimpar	$⊢ (F Fn A \land B \subseteq A) \to B \subseteq dom F$
6		dfss2	$⊢ B \subseteq dom F \leftrightarrow B \cap dom F = B$
7	5 6	sylib	$⊢ (F Fn A \land B \subseteq A) \to B \cap dom F = B$
8	2 7	eqtrid	$⊢ (F Fn A \land B \subseteq A) \to dom F \cap B = B$
9	8	eqeq1d	$⊢ (F Fn A \land B \subseteq A) \to (dom F \cap B = \emptyset \leftrightarrow B = \emptyset)$
10	1 9	bitrid	$⊢ (F Fn A \land B \subseteq A) \to (F [B] = \emptyset \leftrightarrow B = \emptyset)$