Theorem funfvex 5113

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 4833	. 2 |- ( F ` A) = ( iotayA Fy)
2		funfveu 5109	. . 3 |- (( Fun F /\ A e. dom F) -> E!y A Fy)
3		euiotaex 4806	. . 3 |- (E!y A Fy -> ( iotayA Fy) e. _V)
4	2, 3	syl 14	. 2 |- (( Fun F /\ A e. dom F) -> ( iotayA Fy) e. _V)
5	1, 4	syl5eqel 2102	1 |- (( Fun F /\ A e. dom F) -> ( F ` A) e. _V)

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1370  E!weu 1878   _Vcvv 2531   class class class wbr 3734   dom cdm 4268   iotacio 4788   Fun wfun 4819   ` cfv 4825

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-id 4000  df-cnv 4276  df-co 4277  df-dm 4278  df-iota 4790  df-fun 4827  df-fv 4833

This theorem is referenced by:  fnbrfvb  5135  fvelrnb  5142  funimass4  5145  fvelimab  5150  fniinfv  5152  funfvdm  5157  dmfco  5162  fvco2  5163  eqfnfv  5186  fndmdif  5193  fndmin  5195  fvimacnvi  5202  fvimacnv  5203  funconstss  5206  fniniseg  5208  fniniseg2  5210  fnniniseg2  5211  rexsupp  5212  fvelrn  5219  rexrn  5225  ralrn  5226  dff3im  5233  fmptco  5251  fsn2  5258  fnressn  5270  resfunexg  5303  eufnfv  5310  funfvima3  5313  rexima  5315  ralima  5316  fniunfv  5322  elunirn  5326  dff13  5328  foeqcnvco  5351  f1eqcocnv  5352  isocnv2  5373  isoini  5378  f1oiso  5386  fnovex  5458  suppssof1  5647  offveqb  5649  1stexg  5713  2ndexg  5714  smoiso  5835  rdgruledefgg  5878  rdgi0g  5882  rdgivallem  5884  rdg0  5891  frecabex  5895  frectfr  5896