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

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 )