feu

Description: There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003)

		Ref	Expression
	Assertion	feu	$⊢ (F : A ⟶ B \land C \in A) \to \exists! y \in B ⟨C, y⟩ \in F$

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ B \to F Fn A$
2		fneu2	$⊢ (F Fn A \land C \in A) \to \exists! y ⟨C, y⟩ \in F$
3	1 2	sylan	$⊢ (F : A ⟶ B \land C \in A) \to \exists! y ⟨C, y⟩ \in F$
4		opelf	$⊢ (F : A ⟶ B \land ⟨C, y⟩ \in F) \to (C \in A \land y \in B)$
5	4	simprd	$⊢ (F : A ⟶ B \land ⟨C, y⟩ \in F) \to y \in B$
6	5	ex	$⊢ F : A ⟶ B \to (⟨C, y⟩ \in F \to y \in B)$
7	6	pm4.71rd	$⊢ F : A ⟶ B \to (⟨C, y⟩ \in F \leftrightarrow (y \in B \land ⟨C, y⟩ \in F))$
8	7	eubidv	$⊢ F : A ⟶ B \to (\exists! y ⟨C, y⟩ \in F \leftrightarrow \exists! y (y \in B \land ⟨C, y⟩ \in F))$
9	8	adantr	$⊢ (F : A ⟶ B \land C \in A) \to (\exists! y ⟨C, y⟩ \in F \leftrightarrow \exists! y (y \in B \land ⟨C, y⟩ \in F))$
10	3 9	mpbid	$⊢ (F : A ⟶ B \land C \in A) \to \exists! y (y \in B \land ⟨C, y⟩ \in F)$
11		df-reu	$⊢ \exists! y \in B ⟨C, y⟩ \in F \leftrightarrow \exists! y (y \in B \land ⟨C, y⟩ \in F)$
12	10 11	sylibr	$⊢ (F : A ⟶ B \land C \in A) \to \exists! y \in B ⟨C, y⟩ \in F$

Metamath Proof Explorer