Theorem funeu2

Description: There is exactly one value of a function. (Contributed by NM, 3-Aug-1994)

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

Proof

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