Theorem funfvex 5692

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

Syntax hints:   -> wi 4   /\ wa 104   E!weu 2082   e. wcel 2205   _Vcvv 2815   class class class wbr 4114   dom cdm 4754   iotacio 5315   Fun wfun 5351   ` cfv 5357

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 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-id 4419  df-cnv 4762  df-co 4763  df-dm 4764  df-iota 5317  df-fun 5359  df-fv 5365

This theorem is referenced by:  fnbrfvb  5720  fvelrnb  5729  funimass4  5732  fvelimab  5738  fniinfv  5740  funfvdm  5745  dmfco  5750  fvco2  5751  eqfnfv  5780  fndmdif  5788  fndmin  5790  fvimacnvi  5797  fvimacnv  5798  funconstss  5801  fniniseg  5803  fniniseg2  5805  fnniniseg2  5806  fvelrn  5813  rexrn  5819  ralrn  5820  dff3im  5827  fmptco  5848  fsn2  5856  funiun  5864  fnressn  5875  resfunexg  5910  eufnfv  5922  funfvima3  5925  rexima  5933  ralima  5934  fniunfv  5941  elunirn  5945  dff13  5947  foeqcnvco  5969  f1eqcocnv  5970  isocnv2  5991  isoini  5997  f1oiso  6005  fnovex  6091  suppssof1  6293  offveqb  6295  1stexg  6374  2ndexg  6375  smoiso  6546  rdgtfr  6618  rdgruledefgg  6619  rdgivallem  6625  frectfr  6644  frecrdg  6652  en1  7052  fundmen  7060  fnfi  7216  ordiso2  7339  cc2lem  7596  climshft2  12020  slotex  13327  strsetsid  13333  ressbas2d  13369  ressbasid  13371  strressid  13372  ressval3d  13373  imasex  13573  imasival  13574  imasbas  13575  imasplusg  13576  imasmulr  13577  imasaddfn  13585  imasaddval  13586  imasaddf  13587  imasmulfn  13588  imasmulval  13589  imasmulf  13590  qusval  13591  qusex  13593  qusaddvallemg  13601  qusaddflemg  13602  qusaddval  13603  qusaddf  13604  qusmulval  13605  qusmulf  13606  xpsfeq  13613  ismgm  13624  plusffvalg  13629  grpidvalg  13640  fn0g  13642  fngsum  13655  igsumvalx  13656  gsumfzval  13658  gsumress  13662  gsum0g  13663  issgrp  13670  ismnddef  13683  issubmnd  13707  ress0g  13708  ismhm  13720  mhmex  13721  issubm  13731  0mhm  13745  grppropstrg  13778  grpinvfvalg  13801  grpinvval  13802  grpinvfng  13803  grpsubfvalg  13804  grpsubval  13805  grpressid  13820  grplactfval  13860  qusgrp2  13870  mulgfvalg  13878  mulgval  13879  mulgex  13880  mulgfng  13881  issubg  13930  subgex  13933  issubg2m  13946  isnsg  13959  releqgg  13977  eqgex  13978  eqgfval  13979  eqgen  13984  isghm  14000  ablressid  14092  prdsex  14118  prdsval  14119  prdsbaslemss  14120  prdsbas  14122  prdsplusg  14123  prdsmulr  14124  xpsval  14147  pwsbas  14151  pwselbasb  14152  pwssnf1o  14157  mgptopng  14172  isrng  14177  rngressid  14197  qusrng  14201  dfur2g  14209  issrg  14212  isring  14247  ringidss  14276  ringressid  14310  qusring2  14313  dvdsrvald  14342  dvdsrex  14347  unitgrp  14365  unitabl  14366  invrfvald  14371  unitlinv  14375  unitrinv  14376  dvrfvald  14382  rdivmuldivd  14393  invrpropdg  14398  dfrhm2  14403  rhmex  14406  rhmunitinv  14427  isnzr2  14433  issubrng  14449  issubrg  14471  subrgugrp  14490  rrgval  14512  isdomn  14520  aprval  14533  aprap  14540  aprprop  14543  islmod  14569  scaffvalg  14584  rmodislmod  14629  lssex  14632  lsssetm  14634  islssm  14635  islssmg  14636  islss3  14657  lspfval  14666  lspval  14668  lspcl  14669  lspex  14673  sraval  14715  sralemg  14716  srascag  14720  sravscag  14721  sraipg  14722  sraex  14724  rlmsubg  14736  rlmvnegg  14743  ixpsnbasval  14744  lidlex  14751  rspex  14752  lidlss  14754  lidlrsppropdg  14773  qusrhm  14806  mopnset  14830  psrval  14944  fnpsr  14945  psrbasg  14959  psrelbas  14960  psrplusgg  14963  psraddcl  14965  psr0cl  14966  psrnegcl  14968  psr1clfi  14973  mplvalcoe  14975  fnmpl  14978  mplplusgg  14988  vtxvalg  16141  vtxex  16143  eupth2lem3lem6fi  16596