Theorem ffvelcdmd 5844

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypotheses

Ref	Expression
ffvelcdmd.1	|- ( ph -> F : A --> B )
ffvelcdmd.2	|- ( ph -> C e. A )

Assertion

Ref	Expression
ffvelcdmd	|- ( ph -> ( F ` C ) e. B )

Proof of Theorem ffvelcdmd

Step	Hyp	Ref	Expression
1		ffvelcdmd.2	. 2 |- ( ph -> C e. A )
2		ffvelcdmd.1	. . 3 |- ( ph -> F : A --> B )
3	2	ffvelcdmda 5843	. 2 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )
4	1, 3	mpdan 425	1 |- ( ph -> ( F ` C ) e. B )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   -->wf 5373   ` cfv 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-fv 5385

This theorem is used by:  isotr  6022  caofinvl  6328  fvdifsuppst  6484  rdgon  6657  frecabcl  6670  1dom1el  7107  phplem4dom  7163  fidceq  7171  dif1en  7183  fin0  7189  fin0or  7190  infm  7211  en2eqpr  7214  fidcenumlemrks  7270  fidcenumlemr  7272  fdcf1  7316  2omap  7318  supisoti  7350  ordiso2  7375  updjudhcoinlf  7420  updjudhcoinrg  7421  caseinl  7431  caseinr  7432  difinfsnlem  7439  difinfsn  7440  ctmlemr  7448  ctssdclemn0  7450  ctssdc  7453  enumctlemm  7454  enumct  7455  nnnninfeq2  7469  nninfisol  7473  enomnilem  7478  finomni  7480  ismkvnex  7495  enmkvlem  7501  enwomnilem  7509  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  pr2cv1  7541  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acnccim  7638  cauappcvgprlemm  8012  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprlem2  8047  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnbj  8060  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemexb  8074  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  caucvgsr  8169  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  fseq1p1m1  10511  4fvwrd4  10557  fvinim0ffz  10670  frecuzrdgg  10866  frecuzrdgsuctlem  10873  seq3val  10910  seqvalcd  10911  seq3p1  10915  seqp1cd  10920  ser3mono  10937  seq3split  10938  seq3caopr2  10943  iseqf1olemkle  10947  iseqf1olemklt  10948  iseqf1olemqcl  10949  iseqf1olemnab  10951  iseqf1olemmo  10955  iseqf1olemqk  10957  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seq3f1olemstep  10964  seq3f1oleml  10966  seq3f1o  10967  seqf1oglem2a  10968  seqf1oglem1  10969  seqf1oglem2  10970  seq3z  10978  seq3distr  10982  ser3ge0  10986  ser3le  10987  exp3vallem  10990  exp3val  10991  bcval5  11215  hashfz1  11236  resunimafz0  11288  leisorel  11303  zfz1isolemiso  11305  seq3coll  11308  ccatcl  11375  swrdclg  11436  caucvgrelemcau  11760  caucvgre  11761  cvg1nlemf  11763  cvg1nlemcau  11764  cvg1nlemres  11765  recvguniqlem  11774  resqrexlemdecn  11792  resqrexlemcalc3  11796  resqrexlemnmsq  11797  resqrexlemnm  11798  resqrexlemcvg  11799  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemga  11803  clim2ser  12119  clim2ser2  12120  climrecvg1n  12130  climcvg1nlem  12131  serf0  12134  sumeq2  12141  fsum3cvg  12161  summodclem2a  12164  fsum3  12170  fisumss  12175  fsumcl2lem  12181  fsumadd  12189  fsummulc2  12231  fsumrelem  12254  isumshft  12273  cvgratnnlemseq  12309  cvgratnnlemrate  12313  clim2prod  12322  clim2divap  12323  prodfrecap  12329  prodfdivap  12330  ntrivcvgap  12331  prodeq2  12340  fproddccvg  12355  prodmodclem3  12358  prodmodclem2a  12359  fprodseq  12366  fprodssdc  12373  fprodmul  12374  effsumlt  12475  nninfctlemfo  12833  nn0seqcvgd  12835  ialgrlem1st  12836  eulerthlemrprm  13027  eulerthlema  13028  eulerthlemh  13029  pcmpt2  13143  pcmptdvds  13144  1arithlem4  13165  1arith  13166  ennnfonelemdc  13339  ennnfonelemjn  13342  ennnfonelemg  13343  ennnfonelemp1  13346  ennnfonelemom  13348  ennnfonelemhdmp1  13349  ennnfonelemss  13350  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemnn0  13362  ennnfonelemim  13364  ctinfomlemom  13367  ctiunctlemudc  13377  ctiunctlemf  13378  ctiunctlemfo  13379  ssnnctlemct  13386  nninfdclemp1  13390  nninfdclemlt  13391  imasmnd2  13808  mhmf1o  13826  mhmco  13846  gzsumcl  13853  isgrpinv  13908  imasgrp2  13962  mhmid  13967  mhmmnd  13968  ghmgrp  13970  mulgval  13974  mulgfng  13976  mulgnnsubcl  13986  ghmid  14101  ghminv  14102  ghmmulg  14108  ghmnsgpreima  14121  ghmeqker  14123  ghmf1  14125  kerf1ghm  14126  ghmf1o  14127  gzsumsplit0  14197  gsumvalfi  14201  gsumclfi  14208  gsumsubmclfi  14212  pwssub  14265  imasring  14418  rhmopp  14532  lspcl  14777  znidomb  15042  znrrg  15044  asclelbas  15075  psrbaglesuppg  15106  psrbagfi  15108  psrbaglecl  15109  psrbagcon  15111  mplsubgfilemcl  15139  iscnp4  15368  cnptopco  15372  lmtopcnp  15400  upxp  15422  uptx  15424  txlm  15429  comet  15649  metcnp3  15661  metcnp  15662  metcnp2  15663  metcnpi3  15667  elcncf2  15724  cncfco  15741  ivthreinc  15795  limcimolemlt  15814  cnplimcim  15817  cnplimclemle  15818  cnplimclemr  15819  limccnpcntop  15825  dvlemap  15830  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvef  15877  plyaddlem1  15897  plymullem1  15898  plycoeid3  15907  plycolemc  15908  plycjlemc  15910  plycj  15911  plycn  15912  plyrecj  15913  dvply1  15915  dvply2g  15916  logfac  16048  bposlem3  16211  bposlem5  16213  lgsval  16221  lgscllem  16224  lgsval2lem  16227  lgsval4a  16239  lgsneg  16241  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  lgseisenlem3  16289  lgseisenlem4  16290  p1evtxdeqfi  16651  wlkvtxm  16679  wlkvtxiedg  16684  wlkvtxiedgg  16685  upgriswlkdc  16699  trlsegvdeglem7  16805  trlsegvdegfi  16806  eupth2lem3lem1fi  16807  eupth2lem3lem2fi  16808  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  eupth2lem3lem7fi  16813  eupth2lemsfi  16817  3dom  17116  pwle2  17126  subctctexmid  17128  nnsf  17146  peano4nninf  17147  nninfalllem1  17149  nninfsellemdc  17151  nninfsellemeq  17155  nninfsellemqall  17156  nninfsellemeqinf  17157  nninfomnilem  17159  nnnninfex  17163  nninfnfiinf  17164  repiecelem  17172  repiecele0  17173  repiecege0  17174  isomninnlem  17177  trilpolemeq1  17187  trilpolemlt1  17188  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200  nconstwlpolemgt0  17212  nconstwlpolem  17213