Theorem 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	$$⊢\left(F:A⟶B\wedge X\in A\right)\to \exists !y\in BF\left(X\right)=y$$

Proof

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