fdmeu

Description: There is exactly one codomain element for each element of the domain of a function. (Contributed by AV, 20-Apr-2025)

		Ref	Expression
	Assertion	fdmeu	$⊢ (F : A ⟶ B \land X \in A) \to \exists! y \in B F (X) = y$

Step	Hyp	Ref	Expression
1		feu	$⊢ (F : A ⟶ B \land X \in A) \to \exists! y \in B ⟨X, y⟩ \in F$
2		ffn	$⊢ F : A ⟶ B \to F Fn A$
3	2	anim1i	$⊢ (F : A ⟶ B \land X \in A) \to (F Fn A \land X \in A)$
4	3	adantr	$⊢ ((F : A ⟶ B \land X \in A) \land y \in B) \to (F Fn A \land X \in A)$
5		fnopfvb	$⊢ (F Fn A \land X \in A) \to (F (X) = y \leftrightarrow ⟨X, y⟩ \in F)$
6	4 5	syl	$⊢ ((F : A ⟶ B \land X \in A) \land y \in B) \to (F (X) = y \leftrightarrow ⟨X, y⟩ \in F)$
7	6	reubidva	$⊢ (F : A ⟶ B \land X \in A) \to (\exists! y \in B F (X) = y \leftrightarrow \exists! y \in B ⟨X, y⟩ \in F)$
8	1 7	mpbird	$⊢ (F : A ⟶ B \land X \in A) \to \exists! y \in B F (X) = y$

Metamath Proof Explorer