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  12016  slotex  13323  strsetsid  13329  ressbas2d  13365  ressbasid  13367  strressid  13368  ressval3d  13369  prdsex  13566  prdsval  13570  prdsbaslemss  13571  prdsbas  13573  prdsplusg  13574  prdsmulr  13575  pwsbas  13589  pwselbasb  13590  pwssnf1o  13595  imasex  13602  imasival  13603  imasbas  13604  imasplusg  13605  imasmulr  13606  imasaddfn  13614  imasaddval  13615  imasaddf  13616  imasmulfn  13617  imasmulval  13618  imasmulf  13619  qusval  13620  qusex  13622  qusaddvallemg  13630  qusaddflemg  13631  qusaddval  13632  qusaddf  13633  qusmulval  13634  qusmulf  13635  xpsfeq  13642  xpsval  13649  ismgm  13654  plusffvalg  13659  grpidvalg  13670  fn0g  13672  fngsum  13685  igsumvalx  13686  gsumfzval  13688  gsumress  13692  gsum0g  13693  issgrp  13700  ismnddef  13715  issubmnd  13739  ress0g  13740  ismhm  13758  mhmex  13759  issubm  13769  0mhm  13783  grppropstrg  13816  grpinvfvalg  13839  grpinvval  13840  grpinvfng  13841  grpsubfvalg  13842  grpsubval  13843  grpressid  13858  grplactfval  13898  qusgrp2  13914  mulgfvalg  13922  mulgval  13923  mulgex  13924  mulgfng  13925  issubg  13974  subgex  13977  issubg2m  13990  isnsg  14003  releqgg  14021  eqgex  14022  eqgfval  14023  eqgen  14028  isghm  14044  ablressid  14136  mgptopng  14157  isrng  14162  rngressid  14182  qusrng  14186  dfur2g  14190  issrg  14193  isring  14228  ringidss  14257  ringressid  14291  qusring2  14294  dvdsrvald  14323  dvdsrex  14328  unitgrp  14346  unitabl  14347  invrfvald  14352  unitlinv  14356  unitrinv  14357  dvrfvald  14363  rdivmuldivd  14374  invrpropdg  14379  dfrhm2  14384  rhmex  14387  rhmunitinv  14408  isnzr2  14414  issubrng  14430  issubrg  14452  subrgugrp  14471  rrgval  14493  isdomn  14501  aprval  14514  aprap  14521  aprprop  14524  islmod  14551  scaffvalg  14566  rmodislmod  14611  lssex  14614  lsssetm  14616  islssm  14617  islssmg  14618  islss3  14639  lspfval  14648  lspval  14650  lspcl  14651  lspex  14655  sraval  14697  sralemg  14698  srascag  14702  sravscag  14703  sraipg  14704  sraex  14706  rlmsubg  14718  rlmvnegg  14725  ixpsnbasval  14726  lidlex  14733  rspex  14734  lidlss  14736  lidlrsppropdg  14755  qusrhm  14788  mopnset  14812  psrval  14926  fnpsr  14927  psrbasg  14941  psrelbas  14942  psrplusgg  14945  psraddcl  14947  psr0cl  14948  psrnegcl  14950  psr1clfi  14955  mplvalcoe  14957  fnmpl  14960  mplplusgg  14970  vtxvalg  16123  vtxex  16125  eupth2lem3lem6fi  16578