Theorem funfvex 5665

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 5341	. 2 |- ( F ` A ) = ( iota y A F y )
2		funfveu 5661	. . 3 |- ( ( Fun F /\ A e. dom F ) -> E! y A F y )
3		euiotaex 5310	. . 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 2803   class class class wbr 4093   dom cdm 4731   iotacio 5291   Fun wfun 5327   ` cfv 5333

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-id 4396  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fv 5341

This theorem is referenced by:  fnbrfvb  5693  fvelrnb  5702  funimass4  5705  fvelimab  5711  fniinfv  5713  funfvdm  5718  dmfco  5723  fvco2  5724  eqfnfv  5753  fndmdif  5761  fndmin  5763  fvimacnvi  5770  fvimacnv  5771  funconstss  5774  fniniseg  5776  fniniseg2  5778  fnniniseg2  5779  fvelrn  5786  rexrn  5792  ralrn  5793  dff3im  5800  fmptco  5821  fsn2  5829  funiun  5837  fnressn  5848  resfunexg  5883  eufnfv  5895  funfvima3  5898  rexima  5905  ralima  5906  fniunfv  5913  elunirn  5917  dff13  5919  foeqcnvco  5941  f1eqcocnv  5942  isocnv2  5963  isoini  5969  f1oiso  5977  fnovex  6061  suppssof1  6262  offveqb  6264  1stexg  6339  2ndexg  6340  smoiso  6511  rdgtfr  6583  rdgruledefgg  6584  rdgivallem  6590  frectfr  6609  frecrdg  6617  en1  7016  fundmen  7024  fnfi  7178  ordiso2  7277  cc2lem  7528  climshft2  11927  slotex  13170  strsetsid  13176  ressbas2d  13212  ressbasid  13214  strressid  13215  ressval3d  13216  prdsex  13413  prdsval  13417  prdsbaslemss  13418  prdsbas  13420  prdsplusg  13421  prdsmulr  13422  pwsbas  13436  pwselbasb  13437  pwssnf1o  13442  imasex  13449  imasival  13450  imasbas  13451  imasplusg  13452  imasmulr  13453  imasaddfn  13461  imasaddval  13462  imasaddf  13463  imasmulfn  13464  imasmulval  13465  imasmulf  13466  qusval  13467  qusex  13469  qusaddvallemg  13477  qusaddflemg  13478  qusaddval  13479  qusaddf  13480  qusmulval  13481  qusmulf  13482  xpsfeq  13489  xpsval  13496  ismgm  13501  plusffvalg  13506  grpidvalg  13517  fn0g  13519  fngsum  13532  igsumvalx  13533  gsumfzval  13535  gsumress  13539  gsum0g  13540  issgrp  13547  ismnddef  13562  issubmnd  13586  ress0g  13587  ismhm  13605  mhmex  13606  issubm  13616  0mhm  13630  grppropstrg  13663  grpinvfvalg  13686  grpinvval  13687  grpinvfng  13688  grpsubfvalg  13689  grpsubval  13690  grpressid  13705  grplactfval  13745  qusgrp2  13761  mulgfvalg  13769  mulgval  13770  mulgex  13771  mulgfng  13772  issubg  13821  subgex  13824  issubg2m  13837  isnsg  13850  releqgg  13868  eqgex  13869  eqgfval  13870  eqgen  13875  isghm  13891  ablressid  13983  mgptopng  14004  isrng  14009  rngressid  14029  qusrng  14033  dfur2g  14037  issrg  14040  isring  14075  ringidss  14104  ringressid  14138  qusring2  14141  dvdsrvald  14169  dvdsrex  14174  unitgrp  14192  unitabl  14193  invrfvald  14198  unitlinv  14202  unitrinv  14203  dvrfvald  14209  rdivmuldivd  14220  invrpropdg  14225  dfrhm2  14230  rhmex  14233  rhmunitinv  14254  isnzr2  14260  issubrng  14275  issubrg  14297  subrgugrp  14316  rrgval  14338  isdomn  14345  aprval  14358  aprap  14362  islmod  14367  scaffvalg  14382  rmodislmod  14427  lssex  14430  lsssetm  14432  islssm  14433  islssmg  14434  islss3  14455  lspfval  14464  lspval  14466  lspcl  14467  lspex  14471  sraval  14513  sralemg  14514  srascag  14518  sravscag  14519  sraipg  14520  sraex  14522  rlmsubg  14534  rlmvnegg  14541  ixpsnbasval  14542  lidlex  14549  rspex  14550  lidlss  14552  lidlrsppropdg  14571  qusrhm  14604  mopnset  14628  psrval  14742  fnpsr  14743  psrbasg  14755  psrelbas  14756  psrplusgg  14759  psraddcl  14761  psr0cl  14762  psrnegcl  14764  psr1clfi  14769  mplvalcoe  14771  fnmpl  14774  mplplusgg  14784  vtxvalg  15937  vtxex  15939  eupth2lem3lem6fi  16392