This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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