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

Metamath Proof Explorer

Theorem funeu

Description: There is exactly one value of a function. (Contributed by NM, 22-Apr-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion funeu ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ∃! 𝑦 𝐴 𝐹 𝑦 )

Proof

Step Hyp Ref Expression
1 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
2 releldm ⊢ ( ( Rel 𝐹 ∧ 𝐴 𝐹 𝐵 ) → 𝐴 ∈ dom 𝐹 )
3 1 2 sylan ⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → 𝐴 ∈ dom 𝐹 )
4 eldmg ⊢ ( 𝐴 ∈ dom 𝐹 → ( 𝐴 ∈ dom 𝐹 ↔ ∃ 𝑦 𝐴 𝐹 𝑦 ) )
5 4 ibi ⊢ ( 𝐴 ∈ dom 𝐹 → ∃ 𝑦 𝐴 𝐹 𝑦 )
6 3 5 syl ⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ∃ 𝑦 𝐴 𝐹 𝑦 )
7 funmo ⊢ ( Fun 𝐹 → ∃* 𝑦 𝐴 𝐹 𝑦 )
8 7 adantr ⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ∃* 𝑦 𝐴 𝐹 𝑦 )
9 moeu ⊢ ( ∃* 𝑦 𝐴 𝐹 𝑦 ↔ ( ∃ 𝑦 𝐴 𝐹 𝑦 → ∃! 𝑦 𝐴 𝐹 𝑦 ) )
10 8 9 sylib ⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ( ∃ 𝑦 𝐴 𝐹 𝑦 → ∃! 𝑦 𝐴 𝐹 𝑦 ) )
11 6 10 mpd ⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ∃! 𝑦 𝐴 𝐹 𝑦 )