Theorem funfvex 5640

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 5322	. 2 |- ( F ` A ) = ( iota y A F y )
2		funfveu 5636	. . 3 |- ( ( Fun F /\ A e. dom F ) -> E! y A F y )
3		euiotaex 5291	. . 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 2316	1 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   E!weu 2077   e. wcel 2200   _Vcvv 2799   class class class wbr 4082   dom cdm 4716   iotacio 5272   Fun wfun 5308   ` cfv 5314

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-id 4381  df-cnv 4724  df-co 4725  df-dm 4726  df-iota 5274  df-fun 5316  df-fv 5322

This theorem is referenced by:  fnbrfvb  5666  fvelrnb  5674  funimass4  5677  fvelimab  5683  fniinfv  5685  funfvdm  5690  dmfco  5695  fvco2  5696  eqfnfv  5725  fndmdif  5733  fndmin  5735  fvimacnvi  5742  fvimacnv  5743  funconstss  5746  fniniseg  5748  fniniseg2  5750  fnniniseg2  5751  rexsupp  5752  fvelrn  5759  rexrn  5765  ralrn  5766  dff3im  5773  fmptco  5794  fsn2  5802  funiun  5809  fnressn  5818  resfunexg  5853  eufnfv  5863  funfvima3  5866  rexima  5871  ralima  5872  fniunfv  5879  elunirn  5883  dff13  5885  foeqcnvco  5907  f1eqcocnv  5908  isocnv2  5929  isoini  5935  f1oiso  5943  fnovex  6027  suppssof1  6226  offveqb  6228  1stexg  6303  2ndexg  6304  smoiso  6438  rdgtfr  6510  rdgruledefgg  6511  rdgivallem  6517  frectfr  6536  frecrdg  6544  en1  6941  fundmen  6949  fnfi  7091  ordiso2  7190  cc2lem  7440  climshft2  11803  slotex  13045  strsetsid  13051  ressbas2d  13087  ressbasid  13089  strressid  13090  ressval3d  13091  prdsex  13288  prdsval  13292  prdsbaslemss  13293  prdsbas  13295  prdsplusg  13296  prdsmulr  13297  pwsbas  13311  pwselbasb  13312  pwssnf1o  13317  imasex  13324  imasival  13325  imasbas  13326  imasplusg  13327  imasmulr  13328  imasaddfn  13336  imasaddval  13337  imasaddf  13338  imasmulfn  13339  imasmulval  13340  imasmulf  13341  qusval  13342  qusex  13344  qusaddvallemg  13352  qusaddflemg  13353  qusaddval  13354  qusaddf  13355  qusmulval  13356  qusmulf  13357  xpsfeq  13364  xpsval  13371  ismgm  13376  plusffvalg  13381  grpidvalg  13392  fn0g  13394  fngsum  13407  igsumvalx  13408  gsumfzval  13410  gsumress  13414  gsum0g  13415  issgrp  13422  ismnddef  13437  issubmnd  13461  ress0g  13462  ismhm  13480  mhmex  13481  issubm  13491  0mhm  13505  grppropstrg  13538  grpinvfvalg  13561  grpinvval  13562  grpinvfng  13563  grpsubfvalg  13564  grpsubval  13565  grpressid  13580  grplactfval  13620  qusgrp2  13636  mulgfvalg  13644  mulgval  13645  mulgex  13646  mulgfng  13647  issubg  13696  subgex  13699  issubg2m  13712  isnsg  13725  releqgg  13743  eqgex  13744  eqgfval  13745  eqgen  13750  isghm  13766  ablressid  13858  mgptopng  13878  isrng  13883  rngressid  13903  qusrng  13907  dfur2g  13911  issrg  13914  isring  13949  ringidss  13978  ringressid  14012  qusring2  14015  reldvdsrsrg  14041  dvdsrvald  14042  dvdsrex  14047  unitgrp  14065  unitabl  14066  invrfvald  14071  unitlinv  14075  unitrinv  14076  dvrfvald  14082  rdivmuldivd  14093  invrpropdg  14098  dfrhm2  14103  rhmex  14106  rhmunitinv  14127  isnzr2  14133  issubrng  14148  issubrg  14170  subrgugrp  14189  rrgval  14211  isdomn  14218  aprval  14231  aprap  14235  islmod  14240  scaffvalg  14255  rmodislmod  14300  lssex  14303  lsssetm  14305  islssm  14306  islssmg  14307  islss3  14328  lspfval  14337  lspval  14339  lspcl  14340  lspex  14344  sraval  14386  sralemg  14387  srascag  14391  sravscag  14392  sraipg  14393  sraex  14395  rlmsubg  14407  rlmvnegg  14414  ixpsnbasval  14415  lidlex  14422  rspex  14423  lidlss  14425  lidlrsppropdg  14444  qusrhm  14477  mopnset  14501  psrval  14615  fnpsr  14616  psrbasg  14623  psrelbas  14624  psrplusgg  14627  psraddcl  14629  psr0cl  14630  psrnegcl  14632  psr1clfi  14637  mplvalcoe  14639  fnmpl  14642  mplplusgg  14652  vtxvalg  15802  vtxex  15804