Metamath Proof Explorer

Theorem fununiq

Description: The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013)

Ref Expression
Hypotheses fununiq.1 ⊢ A ∈ V
fununiq.2 ⊢ B ∈ V
fununiq.3 ⊢ C ∈ V
Assertion fununiq ⊢ Fun ⁡ F → A F B ∧ A F C → B = C

Proof

Step Hyp Ref Expression
1 fununiq.1 ⊢ A ∈ V
2 fununiq.2 ⊢ B ∈ V
3 fununiq.3 ⊢ C ∈ V
4 dffun2 ⊢ Fun ⁡ F ↔ Rel ⁡ F ∧ ∀ x ∀ y ∀ z x F y ∧ x F z → y = z
5 breq12 ⊢ x = A ∧ y = B → x F y ↔ A F B
6 5 3adant3 ⊢ x = A ∧ y = B ∧ z = C → x F y ↔ A F B
7 breq12 ⊢ x = A ∧ z = C → x F z ↔ A F C
8 7 3adant2 ⊢ x = A ∧ y = B ∧ z = C → x F z ↔ A F C
9 6 8 anbi12d ⊢ x = A ∧ y = B ∧ z = C → x F y ∧ x F z ↔ A F B ∧ A F C
10 eqeq12 ⊢ y = B ∧ z = C → y = z ↔ B = C
11 10 3adant1 ⊢ x = A ∧ y = B ∧ z = C → y = z ↔ B = C
12 9 11 imbi12d ⊢ x = A ∧ y = B ∧ z = C → x F y ∧ x F z → y = z ↔ A F B ∧ A F C → B = C
13 12 spc3gv ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → ∀ x ∀ y ∀ z x F y ∧ x F z → y = z → A F B ∧ A F C → B = C
14 1 2 3 13 mp3an ⊢ ∀ x ∀ y ∀ z x F y ∧ x F z → y = z → A F B ∧ A F C → B = C
15 4 14 simplbiim ⊢ Fun ⁡ F → A F B ∧ A F C → B = C