Theorem fneu

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	fneu	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∃! 𝑦 𝐵 𝐹 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		funmo	⊢ ( Fun 𝐹 → ∃* 𝑦 𝐵 𝐹 𝑦 )
2	1	adantr	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ∃* 𝑦 𝐵 𝐹 𝑦 )
3		eldmg	⊢ ( 𝐵 ∈ dom 𝐹 → ( 𝐵 ∈ dom 𝐹 ↔ ∃ 𝑦 𝐵 𝐹 𝑦 ) )
4	3	ibi	⊢ ( 𝐵 ∈ dom 𝐹 → ∃ 𝑦 𝐵 𝐹 𝑦 )
5	4	adantl	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ∃ 𝑦 𝐵 𝐹 𝑦 )
6		exmoeub	⊢ ( ∃ 𝑦 𝐵 𝐹 𝑦 → ( ∃* 𝑦 𝐵 𝐹 𝑦 ↔ ∃! 𝑦 𝐵 𝐹 𝑦 ) )
7	5 6	syl	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( ∃* 𝑦 𝐵 𝐹 𝑦 ↔ ∃! 𝑦 𝐵 𝐹 𝑦 ) )
8	2 7	mpbid	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ∃! 𝑦 𝐵 𝐹 𝑦 )
9	8	funfni	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∃! 𝑦 𝐵 𝐹 𝑦 )