Metamath Proof Explorer


Theorem fununiq

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

Ref Expression
Hypotheses fununiq.1 𝐴 ∈ V
fununiq.2 𝐵 ∈ V
fununiq.3 𝐶 ∈ V
Assertion fununiq ( Fun 𝐹 → ( ( 𝐴 𝐹 𝐵𝐴 𝐹 𝐶 ) → 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fununiq.1 𝐴 ∈ V
2 fununiq.2 𝐵 ∈ V
3 fununiq.3 𝐶 ∈ V
4 dffun2 ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥𝑦𝑧 ( ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) ) )
5 breq12 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝑥 𝐹 𝑦𝐴 𝐹 𝐵 ) )
6 5 3adant3 ( ( 𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶 ) → ( 𝑥 𝐹 𝑦𝐴 𝐹 𝐵 ) )
7 breq12 ( ( 𝑥 = 𝐴𝑧 = 𝐶 ) → ( 𝑥 𝐹 𝑧𝐴 𝐹 𝐶 ) )
8 7 3adant2 ( ( 𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶 ) → ( 𝑥 𝐹 𝑧𝐴 𝐹 𝐶 ) )
9 6 8 anbi12d ( ( 𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶 ) → ( ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) ↔ ( 𝐴 𝐹 𝐵𝐴 𝐹 𝐶 ) ) )
10 eqeq12 ( ( 𝑦 = 𝐵𝑧 = 𝐶 ) → ( 𝑦 = 𝑧𝐵 = 𝐶 ) )
11 10 3adant1 ( ( 𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶 ) → ( 𝑦 = 𝑧𝐵 = 𝐶 ) )
12 9 11 imbi12d ( ( 𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶 ) → ( ( ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) ↔ ( ( 𝐴 𝐹 𝐵𝐴 𝐹 𝐶 ) → 𝐵 = 𝐶 ) ) )
13 12 spc3gv ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ∀ 𝑥𝑦𝑧 ( ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) → ( ( 𝐴 𝐹 𝐵𝐴 𝐹 𝐶 ) → 𝐵 = 𝐶 ) ) )
14 1 2 3 13 mp3an ( ∀ 𝑥𝑦𝑧 ( ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) → ( ( 𝐴 𝐹 𝐵𝐴 𝐹 𝐶 ) → 𝐵 = 𝐶 ) )
15 4 14 simplbiim ( Fun 𝐹 → ( ( 𝐴 𝐹 𝐵𝐴 𝐹 𝐶 ) → 𝐵 = 𝐶 ) )