Metamath Proof Explorer


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