Theorem fneu2

Description: There is exactly one value of a function. (Contributed by NM, 7-Nov-1995)

	Ref	Expression
Assertion	fneu2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∃! 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fneu	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∃! 𝑦 𝐵 𝐹 𝑦 )
2		df-br	⊢ ( 𝐵 𝐹 𝑦 ↔ ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐹 )
3	2	eubii	⊢ ( ∃! 𝑦 𝐵 𝐹 𝑦 ↔ ∃! 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐹 )
4	1 3	sylib	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ∃! 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐹 )