Theorem funfvex 5686

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 5359	. 2 |- ( F ` A ) = ( iota y A F y )
2		funfveu 5682	. . 3 |- ( ( Fun F /\ A e. dom F ) -> E! y A F y )
3		euiotaex 5328	. . 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	eqeltrid 2319	1 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   E!weu 2080   e. wcel 2203   _Vcvv 2812   class class class wbr 4108   dom cdm 4748   iotacio 5309   Fun wfun 5345   ` cfv 5351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-sbc 3042  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-id 4413  df-cnv 4756  df-co 4757  df-dm 4758  df-iota 5311  df-fun 5353  df-fv 5359

This theorem is referenced by:  fnbrfvb  5714  fvelrnb  5723  funimass4  5726  fvelimab  5732  fniinfv  5734  funfvdm  5739  dmfco  5744  fvco2  5745  eqfnfv  5774  fndmdif  5782  fndmin  5784  fvimacnvi  5791  fvimacnv  5792  funconstss  5795  fniniseg  5797  fniniseg2  5799  fnniniseg2  5800  fvelrn  5807  rexrn  5813  ralrn  5814  dff3im  5821  fmptco  5842  fsn2  5850  funiun  5858  fnressn  5869  resfunexg  5904  eufnfv  5916  funfvima3  5919  rexima  5926  ralima  5927  fniunfv  5934  elunirn  5938  dff13  5940  foeqcnvco  5962  f1eqcocnv  5963  isocnv2  5984  isoini  5990  f1oiso  5998  fnovex  6082  suppssof1  6283  offveqb  6285  1stexg  6360  2ndexg  6361  smoiso  6532  rdgtfr  6604  rdgruledefgg  6605  rdgivallem  6611  frectfr  6630  frecrdg  6638  en1  7038  fundmen  7046  fnfi  7202  ordiso2  7325  cc2lem  7579  climshft2  11987  slotex  13231  strsetsid  13237  ressbas2d  13273  ressbasid  13275  strressid  13276  ressval3d  13277  prdsex  13474  prdsval  13478  prdsbaslemss  13479  prdsbas  13481  prdsplusg  13482  prdsmulr  13483  pwsbas  13497  pwselbasb  13498  pwssnf1o  13503  imasex  13510  imasival  13511  imasbas  13512  imasplusg  13513  imasmulr  13514  imasaddfn  13522  imasaddval  13523  imasaddf  13524  imasmulfn  13525  imasmulval  13526  imasmulf  13527  qusval  13528  qusex  13530  qusaddvallemg  13538  qusaddflemg  13539  qusaddval  13540  qusaddf  13541  qusmulval  13542  qusmulf  13543  xpsfeq  13550  xpsval  13557  ismgm  13562  plusffvalg  13567  grpidvalg  13578  fn0g  13580  fngsum  13593  igsumvalx  13594  gsumfzval  13596  gsumress  13600  gsum0g  13601  issgrp  13608  ismnddef  13623  issubmnd  13647  ress0g  13648  ismhm  13666  mhmex  13667  issubm  13677  0mhm  13691  grppropstrg  13724  grpinvfvalg  13747  grpinvval  13748  grpinvfng  13749  grpsubfvalg  13750  grpsubval  13751  grpressid  13766  grplactfval  13806  qusgrp2  13822  mulgfvalg  13830  mulgval  13831  mulgex  13832  mulgfng  13833  issubg  13882  subgex  13885  issubg2m  13898  isnsg  13911  releqgg  13929  eqgex  13930  eqgfval  13931  eqgen  13936  isghm  13952  ablressid  14044  mgptopng  14065  isrng  14070  rngressid  14090  qusrng  14094  dfur2g  14098  issrg  14101  isring  14136  ringidss  14165  ringressid  14199  qusring2  14202  dvdsrvald  14230  dvdsrex  14235  unitgrp  14253  unitabl  14254  invrfvald  14259  unitlinv  14263  unitrinv  14264  dvrfvald  14270  rdivmuldivd  14281  invrpropdg  14286  dfrhm2  14291  rhmex  14294  rhmunitinv  14315  isnzr2  14321  issubrng  14336  issubrg  14358  subrgugrp  14377  rrgval  14399  isdomn  14407  aprval  14420  aprap  14424  islmod  14431  scaffvalg  14446  rmodislmod  14491  lssex  14494  lsssetm  14496  islssm  14497  islssmg  14498  islss3  14519  lspfval  14528  lspval  14530  lspcl  14531  lspex  14535  sraval  14577  sralemg  14578  srascag  14582  sravscag  14583  sraipg  14584  sraex  14586  rlmsubg  14598  rlmvnegg  14605  ixpsnbasval  14606  lidlex  14613  rspex  14614  lidlss  14616  lidlrsppropdg  14635  qusrhm  14668  mopnset  14692  psrval  14806  fnpsr  14807  psrbasg  14821  psrelbas  14822  psrplusgg  14825  psraddcl  14827  psr0cl  14828  psrnegcl  14830  psr1clfi  14835  mplvalcoe  14837  fnmpl  14840  mplplusgg  14850  vtxvalg  16003  vtxex  16005  eupth2lem3lem6fi  16458