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 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ∃! 𝑦 𝐴 𝐹 𝑦 )