Metamath Proof Explorer


Theorem eufnfv

Description: A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011)

Ref Expression
Hypotheses eufnfv.1 A V
eufnfv.2 B V
Assertion eufnfv ∃! f f Fn A x A f x = B

Proof

Step Hyp Ref Expression
1 eufnfv.1 A V
2 eufnfv.2 B V
3 1 mptex x A B V
4 eqeq2 z = x A B f = z f = x A B
5 4 bibi2d z = x A B f Fn A x A f x = B f = z f Fn A x A f x = B f = x A B
6 5 albidv z = x A B f f Fn A x A f x = B f = z f f Fn A x A f x = B f = x A B
7 3 6 spcev f f Fn A x A f x = B f = x A B z f f Fn A x A f x = B f = z
8 eqid x A B = x A B
9 2 8 fnmpti x A B Fn A
10 fneq1 f = x A B f Fn A x A B Fn A
11 9 10 mpbiri f = x A B f Fn A
12 11 pm4.71ri f = x A B f Fn A f = x A B
13 dffn5 f Fn A f = x A f x
14 eqeq1 f = x A f x f = x A B x A f x = x A B
15 13 14 sylbi f Fn A f = x A B x A f x = x A B
16 fvex f x V
17 16 rgenw x A f x V
18 mpteqb x A f x V x A f x = x A B x A f x = B
19 17 18 ax-mp x A f x = x A B x A f x = B
20 15 19 bitrdi f Fn A f = x A B x A f x = B
21 20 pm5.32i f Fn A f = x A B f Fn A x A f x = B
22 12 21 bitr2i f Fn A x A f x = B f = x A B
23 7 22 mpg z f f Fn A x A f x = B f = z
24 eu6 ∃! f f Fn A x A f x = B z f f Fn A x A f x = B f = z
25 23 24 mpbir ∃! f f Fn A x A f x = B