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 e. _V
eufnfv.2
|- B e. _V
Assertion eufnfv
|- E! f ( f Fn A /\ A. x e. A ( f ` x ) = B )

Proof

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