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	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑋 ) = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		feu	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐵 ⟨ 𝑋 , 𝑦 ⟩ ∈ 𝐹 )
2		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
3	2	anim1i	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
4	3	adantr	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
5		fnopfvb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑦 ↔ ⟨ 𝑋 , 𝑦 ⟩ ∈ 𝐹 ) )
6	4 5	syl	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) = 𝑦 ↔ ⟨ 𝑋 , 𝑦 ⟩ ∈ 𝐹 ) )
7	6	reubidva	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ∃! 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑋 ) = 𝑦 ↔ ∃! 𝑦 ∈ 𝐵 ⟨ 𝑋 , 𝑦 ⟩ ∈ 𝐹 ) )
8	1 7	mpbird	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑋 ) = 𝑦 )