Theorem feu

Description: There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003)

	Ref	Expression
Assertion	feu	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐵 ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
2		fneu2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ∃! 𝑦 ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 )
3	1 2	sylan	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ∃! 𝑦 ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 )
4		opelf	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐶 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
5	4	simprd	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ) → 𝑦 ∈ 𝐵 )
6	5	ex	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 → 𝑦 ∈ 𝐵 ) )
7	6	pm4.71rd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ↔ ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ) ) )
8	7	eubidv	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∃! 𝑦 ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ) ) )
9	8	adantr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( ∃! 𝑦 ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ) ) )
10	3 9	mpbid	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ) )
11		df-reu	⊢ ( ∃! 𝑦 ∈ 𝐵 ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 ) )
12	10 11	sylibr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐵 ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 )