This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐵 ⟨ 𝐶 , 𝑦 ⟩ ∈ 𝐹 )