Theorem fv3 5703

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.)

Assertion

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

Distinct variable groups:   x, y, F   x, A, y

Proof of Theorem fv3

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfv 5685	. . 3 |- ( x e. ( F ` A ) <-> E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) )
2		bi2 190	. . . . . . . . . 10 |- ( ( A F y <-> y = z ) -> ( y = z -> A F y ) )
3	2	alimi 1565	. . . . . . . . 9 |- ( A. y ( A F y <-> y = z ) -> A. y ( y = z -> A F y ) )
4		vex 2919	. . . . . . . . . 10 |- z e. _V
5		breq2 4176	. . . . . . . . . 10 |- ( y = z -> ( A F y <-> A F z ) )
6	4, 5	ceqsalv 2942	. . . . . . . . 9 |- ( A. y ( y = z -> A F y ) <-> A F z )
7	3, 6	sylib 189	. . . . . . . 8 |- ( A. y ( A F y <-> y = z ) -> A F z )
8	7	anim2i 553	. . . . . . 7 |- ( ( x e. z /\ A. y ( A F y <-> y = z ) ) -> ( x e. z /\ A F z ) )
9	8	eximi 1582	. . . . . 6 |- ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> E. z ( x e. z /\ A F z ) )
10		elequ2 1726	. . . . . . . 8 |- ( z = y -> ( x e. z <-> x e. y ) )
11		breq2 4176	. . . . . . . 8 |- ( z = y -> ( A F z <-> A F y ) )
12	10, 11	anbi12d 692	. . . . . . 7 |- ( z = y -> ( ( x e. z /\ A F z ) <-> ( x e. y /\ A F y ) ) )
13	12	cbvexv 2053	. . . . . 6 |- ( E. z ( x e. z /\ A F z ) <-> E. y ( x e. y /\ A F y ) )
14	9, 13	sylib 189	. . . . 5 |- ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> E. y ( x e. y /\ A F y ) )
15		19.40 1616	. . . . . . 7 |- ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> ( E. z x e. z /\ E. z A. y ( A F y <-> y = z ) ) )
16	15	simprd 450	. . . . . 6 |- ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> E. z A. y ( A F y <-> y = z ) )
17		df-eu 2258	. . . . . 6 |- ( E! y A F y <-> E. z A. y ( A F y <-> y = z ) )
18	16, 17	sylibr 204	. . . . 5 |- ( E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) -> E! y A F y )
19	14, 18	jca 519	. . . 4 |- ( 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 ) )
20		nfeu1 2264	. . . . . . 7 |- F/ y E! y A F y
21		nfv 1626	. . . . . . . . 9 |- F/ y x e. z
22		nfa1 1802	. . . . . . . . 9 |- F/ y A. y ( A F y <-> y = z )
23	21, 22	nfan 1842	. . . . . . . 8 |- F/ y ( x e. z /\ A. y ( A F y <-> y = z ) )
24	23	nfex 1861	. . . . . . 7 |- F/ y E. z ( x e. z /\ A. y ( A F y <-> y = z ) )
25	20, 24	nfim 1828	. . . . . 6 |- F/ y ( E! y A F y -> E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) )
26		bi1 179	. . . . . . . . . . . . . 14 |- ( ( A F y <-> y = z ) -> ( A F y -> y = z ) )
27		ax-14 1725	. . . . . . . . . . . . . 14 |- ( y = z -> ( x e. y -> x e. z ) )
28	26, 27	syl6 31	. . . . . . . . . . . . 13 |- ( ( A F y <-> y = z ) -> ( A F y -> ( x e. y -> x e. z ) ) )
29	28	com23 74	. . . . . . . . . . . 12 |- ( ( A F y <-> y = z ) -> ( x e. y -> ( A F y -> x e. z ) ) )
30	29	imp3a 421	. . . . . . . . . . 11 |- ( ( A F y <-> y = z ) -> ( ( x e. y /\ A F y ) -> x e. z ) )
31	30	sps 1766	. . . . . . . . . 10 |- ( A. y ( A F y <-> y = z ) -> ( ( x e. y /\ A F y ) -> x e. z ) )
32	31	anc2ri 542	. . . . . . . . 9 |- ( A. y ( A F y <-> y = z ) -> ( ( x e. y /\ A F y ) -> ( x e. z /\ A. y ( A F y <-> y = z ) ) ) )
33	32	com12 29	. . . . . . . 8 |- ( ( x e. y /\ A F y ) -> ( A. y ( A F y <-> y = z ) -> ( x e. z /\ A. y ( A F y <-> y = z ) ) ) )
34	33	eximdv 1629	. . . . . . 7 |- ( ( 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 ) ) ) )
35	17, 34	syl5bi 209	. . . . . 6 |- ( ( x e. y /\ A F y ) -> ( E! y A F y -> E. z ( x e. z /\ A. y ( A F y <-> y = z ) ) ) )
36	25, 35	exlimi 1817	. . . . 5 |- ( 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 ) ) ) )
37	36	imp 419	. . . 4 |- ( ( 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 ) ) )
38	19, 37	impbii 181	. . 3 |- ( 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 ) )
39	1, 38	bitri 241	. 2 |- ( x e. ( F ` A ) <-> ( E. y ( x e. y /\ A F y ) /\ E! y A F y ) )
40	39	abbi2i 2515	1 |- ( F ` A ) = { x | ( E. y ( x e. y /\ A F y ) /\ E! y A F y ) }

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   A.wal 1546   E.wex 1547   = wceq 1649   e. wcel 1721   E!weu 2254   {cab 2390   class class class wbr 4172   ` cfv 5413

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421