Theorem funfvex 5306

Description: The value of a function exists. A special case of Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by Jim Kingdon, 29-Dec-2018.)

Assertion

Ref	Expression
funfvex	|- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. _V )

Proof of Theorem funfvex

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fv 5010	. 2 |- ( F ` A ) = ( iota y A F y )
2		funfveu 5302	. . 3 |- ( ( Fun F /\ A e. dom F ) -> E! y A F y )
3		euiotaex 4983	. . 3 |- ( E! y A F y -> ( iota y A F y ) e. _V )
4	2, 3	syl 14	. 2 |- ( ( Fun F /\ A e. dom F ) -> ( iota y A F y ) e. _V )
5	1, 4	syl5eqel 2174	1 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. _V )

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1438   E!weu 1948   _Vcvv 2619   class class class wbr 3837   dom cdm 4428   iotacio 4965   Fun wfun 4996   ` cfv 5002

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-sbc 2839  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-id 4111  df-cnv 4436  df-co 4437  df-dm 4438  df-iota 4967  df-fun 5004  df-fv 5010

This theorem is referenced by:  fnbrfvb  5329  fvelrnb  5336  funimass4  5339  fvelimab  5344  fniinfv  5346  funfvdm  5351  dmfco  5356  fvco2  5357  eqfnfv  5381  fndmdif  5388  fndmin  5390  fvimacnvi  5397  fvimacnv  5398  funconstss  5401  fniniseg  5403  fniniseg2  5405  fnniniseg2  5406  rexsupp  5407  fvelrn  5414  rexrn  5420  ralrn  5421  dff3im  5428  fmptco  5448  fsn2  5455  fnressn  5467  resfunexg  5500  eufnfv  5507  funfvima3  5510  rexima  5516  ralima  5517  fniunfv  5523  elunirn  5527  dff13  5529  foeqcnvco  5551  f1eqcocnv  5552  isocnv2  5573  isoini  5579  f1oiso  5587  fnovex  5664  suppssof1  5854  offveqb  5856  1stexg  5920  2ndexg  5921  smoiso  6049  rdgtfr  6121  rdgruledefgg  6122  rdgivallem  6128  frectfr  6147  frecrdg  6155  en1  6496  fundmen  6503  fnfi  6625  ordiso2  6707  climshft2  10659