Theorem funfvex 5605

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 5287	. 2 |- ( F ` A ) = ( iota y A F y )
2		funfveu 5601	. . 3 |- ( ( Fun F /\ A e. dom F ) -> E! y A F y )
3		euiotaex 5256	. . 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 2293	1 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   E!weu 2055   e. wcel 2177   _Vcvv 2773   class class class wbr 4050   dom cdm 4682   iotacio 5238   Fun wfun 5273   ` cfv 5279

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4169  ax-pow 4225  ax-pr 4260

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-sbc 3003  df-un 3174  df-in 3176  df-ss 3183  df-pw 3622  df-sn 3643  df-pr 3644  df-op 3646  df-uni 3856  df-br 4051  df-opab 4113  df-id 4347  df-cnv 4690  df-co 4691  df-dm 4692  df-iota 5240  df-fun 5281  df-fv 5287

This theorem is referenced by:  fnbrfvb  5631  fvelrnb  5638  funimass4  5641  fvelimab  5647  fniinfv  5649  funfvdm  5654  dmfco  5659  fvco2  5660  eqfnfv  5689  fndmdif  5697  fndmin  5699  fvimacnvi  5706  fvimacnv  5707  funconstss  5710  fniniseg  5712  fniniseg2  5714  fnniniseg2  5715  rexsupp  5716  fvelrn  5723  rexrn  5729  ralrn  5730  dff3im  5737  fmptco  5758  fsn2  5766  funiun  5773  fnressn  5782  resfunexg  5817  eufnfv  5827  funfvima3  5830  rexima  5835  ralima  5836  fniunfv  5843  elunirn  5847  dff13  5849  foeqcnvco  5871  f1eqcocnv  5872  isocnv2  5893  isoini  5899  f1oiso  5907  fnovex  5989  suppssof1  6188  offveqb  6190  1stexg  6265  2ndexg  6266  smoiso  6400  rdgtfr  6472  rdgruledefgg  6473  rdgivallem  6479  frectfr  6498  frecrdg  6506  en1  6903  fundmen  6911  fnfi  7052  ordiso2  7151  cc2lem  7393  climshft2  11687  slotex  12929  strsetsid  12935  ressbas2d  12970  ressbasid  12972  strressid  12973  ressval3d  12974  prdsex  13171  prdsval  13175  prdsbaslemss  13176  prdsbas  13178  prdsplusg  13179  prdsmulr  13180  pwsbas  13194  pwselbasb  13195  pwssnf1o  13200  imasex  13207  imasival  13208  imasbas  13209  imasplusg  13210  imasmulr  13211  imasaddfn  13219  imasaddval  13220  imasaddf  13221  imasmulfn  13222  imasmulval  13223  imasmulf  13224  qusval  13225  qusex  13227  qusaddvallemg  13235  qusaddflemg  13236  qusaddval  13237  qusaddf  13238  qusmulval  13239  qusmulf  13240  xpsfeq  13247  xpsval  13254  ismgm  13259  plusffvalg  13264  grpidvalg  13275  fn0g  13277  fngsum  13290  igsumvalx  13291  gsumfzval  13293  gsumress  13297  gsum0g  13298  issgrp  13305  ismnddef  13320  issubmnd  13344  ress0g  13345  ismhm  13363  mhmex  13364  issubm  13374  0mhm  13388  grppropstrg  13421  grpinvfvalg  13444  grpinvval  13445  grpinvfng  13446  grpsubfvalg  13447  grpsubval  13448  grpressid  13463  grplactfval  13503  qusgrp2  13519  mulgfvalg  13527  mulgval  13528  mulgex  13529  mulgfng  13530  issubg  13579  subgex  13582  issubg2m  13595  isnsg  13608  releqgg  13626  eqgex  13627  eqgfval  13628  eqgen  13633  isghm  13649  ablressid  13741  mgptopng  13761  isrng  13766  rngressid  13786  qusrng  13790  dfur2g  13794  issrg  13797  isring  13832  ringidss  13861  ringressid  13895  qusring2  13898  reldvdsrsrg  13924  dvdsrvald  13925  dvdsrex  13930  unitgrp  13948  unitabl  13949  invrfvald  13954  unitlinv  13958  unitrinv  13959  dvrfvald  13965  rdivmuldivd  13976  invrpropdg  13981  dfrhm2  13986  rhmex  13989  rhmunitinv  14010  isnzr2  14016  issubrng  14031  issubrg  14053  subrgugrp  14072  rrgval  14094  isdomn  14101  aprval  14114  aprap  14118  islmod  14123  scaffvalg  14138  rmodislmod  14183  lssex  14186  lsssetm  14188  islssm  14189  islssmg  14190  islss3  14211  lspfval  14220  lspval  14222  lspcl  14223  lspex  14227  sraval  14269  sralemg  14270  srascag  14274  sravscag  14275  sraipg  14276  sraex  14278  rlmsubg  14290  rlmvnegg  14297  ixpsnbasval  14298  lidlex  14305  rspex  14306  lidlss  14308  lidlrsppropdg  14327  qusrhm  14360  mopnset  14384  psrval  14498  fnpsr  14499  psrbasg  14506  psrelbas  14507  psrplusgg  14510  psraddcl  14512  psr0cl  14513  psrnegcl  14515  psr1clfi  14520  mplvalcoe  14522  fnmpl  14525  mplplusgg  14535  vtxvalg  15685  vtxex  15687