Metamath Proof Explorer

Theorem fv3

Description: Alternate definition of the value of a function. Definition 6.11 of TakeutiZaring p. 26. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion fv3 
|- ( F ` A ) = { x | ( E. y ( x e. y /\ A F y ) /\ E! y A F y ) }

Proof

Step Hyp Ref Expression
1 elfv 
 |-  ( x e. ( F ` A ) <-> E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) )
2 biimpr 
 |-  ( ( A F y <-> y = z ) -> ( y = z -> A F y ) )
3 2 alimi 
 |-  ( A. y ( A F y <-> y = z ) -> A. y ( y = z -> A F y ) )
4 breq2 
 |-  ( y = z -> ( A F y <-> A F z ) )
5 4 equsalvw 
 |-  ( A. y ( y = z -> A F y ) <-> A F z )
6 3 5 sylib 
 |-  ( A. y ( A F y <-> y = z ) -> A F z )
7 6 anim2i 
 |-  ( ( x e. z /\ A. y ( A F y <-> y = z ) ) -> ( x e. z /\ A F z ) )
8 7 eximi 
 |-  ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> E. z ( x e. z /\ A F z ) )
9 elequ2 
 |-  ( z = y -> ( x e. z <-> x e. y ) )
10 breq2 
 |-  ( z = y -> ( A F z <-> A F y ) )
11 9 10 anbi12d 
 |-  ( z = y -> ( ( x e. z /\ A F z ) <-> ( x e. y /\ A F y ) ) )
12 11 cbvexvw 
 |-  ( E. z ( x e. z /\ A F z ) <-> E. y ( x e. y /\ A F y ) )
13 8 12 sylib 
 |-  ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> E. y ( x e. y /\ A F y ) )
14 exsimpr 
 |-  ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> E. z A. y ( A F y <-> y = z ) )
15 eu6 
 |-  ( E! y A F y <-> E. z A. y ( A F y <-> y = z ) )
16 14 15 sylibr 
 |-  ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> E! y A F y )
17 13 16 jca 
 |-  ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> ( E. y ( x e. y /\ A F y ) /\ E! y A F y ) )
18 nfeu1 
 |-  F/ y E! y A F y
19 nfv 
 |-  F/ y x e. z
20 nfa1 
 |-  F/ y A. y ( A F y <-> y = z )
21 19 20 nfan 
 |-  F/ y ( x e. z /\ A. y ( A F y <-> y = z ) )
22 21 nfex 
 |-  F/ y E. z ( x e. z /\ A. y ( A F y <-> y = z ) )
23 18 22 nfim 
 |-  F/ y ( E! y A F y -> E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) )
24 biimp 
 |-  ( ( A F y <-> y = z ) -> ( A F y -> y = z ) )
25 ax9 
 |-  ( y = z -> ( x e. y -> x e. z ) )
26 24 25 syl6 
 |-  ( ( A F y <-> y = z ) -> ( A F y -> ( x e. y -> x e. z ) ) )
27 26 impcomd 
 |-  ( ( A F y <-> y = z ) -> ( ( x e. y /\ A F y ) -> x e. z ) )
28 27 sps 
 |-  ( A. y ( A F y <-> y = z ) -> ( ( x e. y /\ A F y ) -> x e. z ) )
29 28 anc2ri 
 |-  ( A. y ( A F y <-> y = z ) -> ( ( x e. y /\ A F y ) -> ( x e. z /\ A. y ( A F y <-> y = z ) ) ) )
30 29 com12 
 |-  ( ( x e. y /\ A F y ) -> ( A. y ( A F y <-> y = z ) -> ( x e. z /\ A. y ( A F y <-> y = z ) ) ) )
31 30 eximdv 
 |-  ( ( x e. y /\ A F y ) -> ( E. z A. y ( A F y <-> y = z ) -> E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) ) )
32 15 31 biimtrid 
 |-  ( ( x e. y /\ A F y ) -> ( E! y A F y -> E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) ) )
33 23 32 exlimi 
 |-  ( E. y ( x e. y /\ A F y ) -> ( E! y A F y -> E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) ) )
34 33 imp 
 |-  ( ( E. y ( x e. y /\ A F y ) /\ E! y A F y ) -> E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) )
35 17 34 impbii 
 |-  ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) <-> ( E. y ( x e. y /\ A F y ) /\ E! y A F y ) )
36 1 35 bitri 
 |-  ( x e. ( F ` A ) <-> ( E. y ( x e. y /\ A F y ) /\ E! y A F y ) )
37 36 eqabi 
 |-  ( F ` A ) = { x | ( E. y ( x e. y /\ A F y ) /\ E! y A F y ) }