Metamath Proof Explorer

Theorem funeldmb

Description: If (/) is not part of the range of a function F , then A is in the domain of F iff ( FA ) =/= (/) . (Contributed by Scott Fenton, 7-Dec-2021)

		Ref	Expression
	Assertion	funeldmb	$⊢ (Fun F \land \neg \emptyset \in ran F) \to (A \in dom F \leftrightarrow F (A) \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		fvelrn	$⊢ (Fun F \land A \in dom F) \to F (A) \in ran F$
2	1	ex	$⊢ Fun F \to (A \in dom F \to F (A) \in ran F)$
3	2	adantr	$⊢ (Fun F \land F (A) = \emptyset) \to (A \in dom F \to F (A) \in ran F)$
4		eleq1	$⊢ F (A) = \emptyset \to (F (A) \in ran F \leftrightarrow \emptyset \in ran F)$
5	4	adantl	$⊢ (Fun F \land F (A) = \emptyset) \to (F (A) \in ran F \leftrightarrow \emptyset \in ran F)$
6	3 5	sylibd	$⊢ (Fun F \land F (A) = \emptyset) \to (A \in dom F \to \emptyset \in ran F)$
7	6	con3d	$⊢ (Fun F \land F (A) = \emptyset) \to (\neg \emptyset \in ran F \to \neg A \in dom F)$
8	7	impancom	$⊢ (Fun F \land \neg \emptyset \in ran F) \to (F (A) = \emptyset \to \neg A \in dom F)$
9		ndmfv	$⊢ \neg A \in dom F \to F (A) = \emptyset$
10	8 9	impbid1	$⊢ (Fun F \land \neg \emptyset \in ran F) \to (F (A) = \emptyset \leftrightarrow \neg A \in dom F)$
11	10	necon2abid	$⊢ (Fun F \land \neg \emptyset \in ran F) \to (A \in dom F \leftrightarrow F (A) \neq \emptyset)$