Theorem funfvex 5656

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 5334	. 2 |- ( F ` A ) = ( iota y A F y )
2		funfveu 5652	. . 3 |- ( ( Fun F /\ A e. dom F ) -> E! y A F y )
3		euiotaex 5303	. . 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 2318	1 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   E!weu 2079   e. wcel 2202   _Vcvv 2802   class class class wbr 4088   dom cdm 4725   iotacio 5284   Fun wfun 5320   ` cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334

This theorem is referenced by:  fnbrfvb  5684  fvelrnb  5693  funimass4  5696  fvelimab  5702  fniinfv  5704  funfvdm  5709  dmfco  5714  fvco2  5715  eqfnfv  5744  fndmdif  5752  fndmin  5754  fvimacnvi  5761  fvimacnv  5762  funconstss  5765  fniniseg  5767  fniniseg2  5769  fnniniseg2  5770  rexsupp  5771  fvelrn  5778  rexrn  5784  ralrn  5785  dff3im  5792  fmptco  5813  fsn2  5821  funiun  5829  fnressn  5840  resfunexg  5875  eufnfv  5885  funfvima3  5888  rexima  5895  ralima  5896  fniunfv  5903  elunirn  5907  dff13  5909  foeqcnvco  5931  f1eqcocnv  5932  isocnv2  5953  isoini  5959  f1oiso  5967  fnovex  6051  suppssof1  6253  offveqb  6255  1stexg  6330  2ndexg  6331  smoiso  6468  rdgtfr  6540  rdgruledefgg  6541  rdgivallem  6547  frectfr  6566  frecrdg  6574  en1  6973  fundmen  6981  fnfi  7135  ordiso2  7234  cc2lem  7485  climshft2  11871  slotex  13114  strsetsid  13120  ressbas2d  13156  ressbasid  13158  strressid  13159  ressval3d  13160  prdsex  13357  prdsval  13361  prdsbaslemss  13362  prdsbas  13364  prdsplusg  13365  prdsmulr  13366  pwsbas  13380  pwselbasb  13381  pwssnf1o  13386  imasex  13393  imasival  13394  imasbas  13395  imasplusg  13396  imasmulr  13397  imasaddfn  13405  imasaddval  13406  imasaddf  13407  imasmulfn  13408  imasmulval  13409  imasmulf  13410  qusval  13411  qusex  13413  qusaddvallemg  13421  qusaddflemg  13422  qusaddval  13423  qusaddf  13424  qusmulval  13425  qusmulf  13426  xpsfeq  13433  xpsval  13440  ismgm  13445  plusffvalg  13450  grpidvalg  13461  fn0g  13463  fngsum  13476  igsumvalx  13477  gsumfzval  13479  gsumress  13483  gsum0g  13484  issgrp  13491  ismnddef  13506  issubmnd  13530  ress0g  13531  ismhm  13549  mhmex  13550  issubm  13560  0mhm  13574  grppropstrg  13607  grpinvfvalg  13630  grpinvval  13631  grpinvfng  13632  grpsubfvalg  13633  grpsubval  13634  grpressid  13649  grplactfval  13689  qusgrp2  13705  mulgfvalg  13713  mulgval  13714  mulgex  13715  mulgfng  13716  issubg  13765  subgex  13768  issubg2m  13781  isnsg  13794  releqgg  13812  eqgex  13813  eqgfval  13814  eqgen  13819  isghm  13835  ablressid  13927  mgptopng  13948  isrng  13953  rngressid  13973  qusrng  13977  dfur2g  13981  issrg  13984  isring  14019  ringidss  14048  ringressid  14082  qusring2  14085  dvdsrvald  14113  dvdsrex  14118  unitgrp  14136  unitabl  14137  invrfvald  14142  unitlinv  14146  unitrinv  14147  dvrfvald  14153  rdivmuldivd  14164  invrpropdg  14169  dfrhm2  14174  rhmex  14177  rhmunitinv  14198  isnzr2  14204  issubrng  14219  issubrg  14241  subrgugrp  14260  rrgval  14282  isdomn  14289  aprval  14302  aprap  14306  islmod  14311  scaffvalg  14326  rmodislmod  14371  lssex  14374  lsssetm  14376  islssm  14377  islssmg  14378  islss3  14399  lspfval  14408  lspval  14410  lspcl  14411  lspex  14415  sraval  14457  sralemg  14458  srascag  14462  sravscag  14463  sraipg  14464  sraex  14466  rlmsubg  14478  rlmvnegg  14485  ixpsnbasval  14486  lidlex  14493  rspex  14494  lidlss  14496  lidlrsppropdg  14515  qusrhm  14548  mopnset  14572  psrval  14686  fnpsr  14687  psrbasg  14694  psrelbas  14695  psrplusgg  14698  psraddcl  14700  psr0cl  14701  psrnegcl  14703  psr1clfi  14708  mplvalcoe  14710  fnmpl  14713  mplplusgg  14723  vtxvalg  15873  vtxex  15875  eupth2lem3lem6fi  16328