Theorem funfvex 5551

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 5243	. 2 |- ( F ` A ) = ( iota y A F y )
2		funfveu 5547	. . 3 |- ( ( Fun F /\ A e. dom F ) -> E! y A F y )
3		euiotaex 5212	. . 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 2276	1 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   E!weu 2038   e. wcel 2160   _Vcvv 2752   class class class wbr 4018   dom cdm 4644   iotacio 5194   Fun wfun 5229   ` cfv 5235

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-id 4311  df-cnv 4652  df-co 4653  df-dm 4654  df-iota 5196  df-fun 5237  df-fv 5243

This theorem is referenced by:  fnbrfvb  5577  fvelrnb  5584  funimass4  5587  fvelimab  5593  fniinfv  5595  funfvdm  5600  dmfco  5605  fvco2  5606  eqfnfv  5634  fndmdif  5642  fndmin  5644  fvimacnvi  5651  fvimacnv  5652  funconstss  5655  fniniseg  5657  fniniseg2  5659  fnniniseg2  5660  rexsupp  5661  fvelrn  5668  rexrn  5674  ralrn  5675  dff3im  5682  fmptco  5703  fsn2  5711  fnressn  5723  resfunexg  5758  eufnfv  5768  funfvima3  5771  rexima  5776  ralima  5777  fniunfv  5784  elunirn  5788  dff13  5790  foeqcnvco  5812  f1eqcocnv  5813  isocnv2  5834  isoini  5840  f1oiso  5848  fnovex  5930  suppssof1  6125  offveqb  6127  1stexg  6193  2ndexg  6194  smoiso  6328  rdgtfr  6400  rdgruledefgg  6401  rdgivallem  6407  frectfr  6426  frecrdg  6434  en1  6826  fundmen  6833  fnfi  6967  ordiso2  7065  cc2lem  7296  climshft2  11349  slotex  12542  strsetsid  12548  ressbas2d  12583  ressbasid  12585  strressid  12586  ressval3d  12587  prdsex  12777  imasex  12785  imasival  12786  imasbas  12787  imasplusg  12788  imasmulr  12789  imasaddfn  12797  imasaddval  12798  imasaddf  12799  imasmulfn  12800  imasmulval  12801  imasmulf  12802  qusval  12803  qusex  12805  qusaddvallemg  12812  qusaddflemg  12813  qusaddval  12814  qusaddf  12815  qusmulval  12816  qusmulf  12817  xpsfeq  12824  xpsval  12831  ismgm  12836  plusffvalg  12841  grpidvalg  12852  fn0g  12854  fngsum  12867  igsumvalx  12868  gsumress  12873  gsum0g  12874  issgrp  12881  ismnddef  12894  issubmnd  12918  ress0g  12919  ismhm  12928  mhmex  12929  issubm  12939  0mhm  12953  grppropstrg  12979  grpinvfvalg  13001  grpinvval  13002  grpinvfng  13003  grpsubfvalg  13004  grpsubval  13005  grpressid  13020  grplactfval  13060  qusgrp2  13070  mulgfvalg  13078  mulgval  13079  mulgex  13080  mulgfng  13081  issubg  13129  subgex  13132  issubg2m  13145  isnsg  13158  releqgg  13176  eqgex  13177  eqgfval  13178  eqgen  13183  isghm  13199  ablressid  13289  mgptopng  13300  isrng  13305  rngressid  13325  qusrng  13329  dfur2g  13333  issrg  13336  isring  13371  ringidss  13400  ringressid  13430  qusring2  13433  reldvdsrsrg  13459  dvdsrvald  13460  dvdsrex  13465  unitgrp  13483  unitabl  13484  invrfvald  13489  unitlinv  13493  unitrinv  13494  dvrfvald  13500  rdivmuldivd  13511  invrpropdg  13516  dfrhm2  13521  rhmex  13524  rhmunitinv  13545  issubrng  13563  issubrg  13585  subrgugrp  13604  aprval  13615  aprap  13619  islmod  13624  scaffvalg  13639  rmodislmod  13684  lssex  13687  lsssetm  13689  islssm  13690  islssmg  13691  islss3  13712  lspfval  13721  lspval  13723  lspcl  13724  lspex  13728  sraval  13770  sralemg  13771  srascag  13775  sravscag  13776  sraipg  13777  sraex  13779  rlmsubg  13791  rlmvnegg  13798  ixpsnbasval  13799  lidlex  13806  rspex  13807  lidlss  13809  lidlrsppropdg  13828  psrval  13961  fnpsr  13962  psrbasg  13968  psrelbas  13969  psrplusgg  13971  psraddcl  13973