Theorem ffvelcdmd 5835

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 5834	. 2 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )
4	1, 3	mpdan 425	1 |- ( ph -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   e. wcel 2209   -->wf 5368   ` cfv 5372

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 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 4244  ax-pow 4306  ax-pr 4341

This theorem 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 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-opab 4188  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-fv 5380

This theorem is referenced by:  isotr  6012  caofinvl  6318  fvdifsuppst  6474  rdgon  6647  frecabcl  6660  1dom1el  7097  phplem4dom  7153  fidceq  7161  dif1en  7173  fin0  7179  fin0or  7180  infm  7201  en2eqpr  7204  fidcenumlemrks  7260  fidcenumlemr  7262  fdcf1  7306  2omap  7308  supisoti  7340  ordiso2  7365  updjudhcoinlf  7410  updjudhcoinrg  7411  caseinl  7421  caseinr  7422  difinfsnlem  7429  difinfsn  7430  ctmlemr  7438  ctssdclemn0  7440  ctssdc  7443  enumctlemm  7444  enumct  7445  nnnninfeq2  7459  nninfisol  7463  enomnilem  7468  finomni  7470  ismkvnex  7485  enmkvlem  7491  enwomnilem  7499  nninfwlpoimlemg  7505  nninfwlpoimlemginf  7506  pr2cv1  7531  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  acnccim  7628  cauappcvgprlemm  8002  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdfu  8011  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlem2  8017  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem1  8036  caucvgprlem2  8037  caucvgprprlemnkltj  8046  caucvgprprlemnkeqj  8047  caucvgprprlemnbj  8050  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemloc  8060  caucvgprprlemexbt  8063  caucvgprprlemexb  8064  caucvgprprlemaddq  8065  caucvgprprlem1  8066  caucvgprprlem2  8067  caucvgsrlemcau  8150  caucvgsrlemgt1  8152  caucvgsrlemoffcau  8155  caucvgsrlemoffres  8157  caucvgsr  8159  axcaucvglemval  8254  axcaucvglemcau  8255  axcaucvglemres  8256  fseq1p1m1  10479  4fvwrd4  10525  fvinim0ffz  10638  frecuzrdgg  10831  frecuzrdgsuctlem  10838  seq3val  10875  seqvalcd  10876  seq3p1  10880  seqp1cd  10885  ser3mono  10902  seq3split  10903  seq3caopr2  10908  iseqf1olemkle  10912  iseqf1olemklt  10913  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemmo  10920  iseqf1olemqk  10922  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  iseqf1olemfvp  10925  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  seq3f1olemstep  10929  seq3f1oleml  10931  seq3f1o  10932  seqf1oglem2a  10933  seqf1oglem1  10934  seqf1oglem2  10935  seq3z  10943  seq3distr  10947  ser3ge0  10951  ser3le  10952  exp3vallem  10955  exp3val  10956  bcval5  11179  hashfz1  11200  resunimafz0  11252  leisorel  11267  zfz1isolemiso  11269  seq3coll  11272  ccatcl  11339  swrdclg  11400  caucvgrelemcau  11724  caucvgre  11725  cvg1nlemf  11727  cvg1nlemcau  11728  cvg1nlemres  11729  recvguniqlem  11738  resqrexlemdecn  11756  resqrexlemcalc3  11760  resqrexlemnmsq  11761  resqrexlemnm  11762  resqrexlemcvg  11763  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemga  11767  clim2ser  12081  clim2ser2  12082  climrecvg1n  12092  climcvg1nlem  12093  serf0  12096  sumeq2  12103  fsum3cvg  12123  summodclem2a  12126  fsum3  12132  fisumss  12137  fsumcl2lem  12143  fsumadd  12151  fsummulc2  12193  fsumrelem  12216  isumshft  12235  cvgratnnlemseq  12271  cvgratnnlemrate  12275  clim2prod  12284  clim2divap  12285  prodfrecap  12291  prodfdivap  12292  ntrivcvgap  12293  prodeq2  12302  fproddccvg  12317  prodmodclem3  12320  prodmodclem2a  12321  fprodseq  12328  fprodssdc  12335  fprodmul  12336  effsumlt  12437  nninfctlemfo  12795  nn0seqcvgd  12797  ialgrlem1st  12798  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  pcmpt2  13101  pcmptdvds  13102  1arithlem4  13123  1arith  13124  ennnfonelemdc  13268  ennnfonelemjn  13271  ennnfonelemg  13272  ennnfonelemp1  13275  ennnfonelemom  13277  ennnfonelemhdmp1  13278  ennnfonelemss  13279  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemnn0  13291  ennnfonelemim  13293  ctinfomlemom  13296  ctiunctlemudc  13306  ctiunctlemf  13307  ctiunctlemfo  13308  ssnnctlemct  13315  nninfdclemp1  13319  nninfdclemlt  13320  imasmnd2  13736  mhmf1o  13754  mhmco  13774  gzsumcl  13781  isgrpinv  13836  imasgrp2  13890  mhmid  13895  mhmmnd  13896  ghmgrp  13898  mulgval  13902  mulgfng  13904  mulgnnsubcl  13914  ghmid  14029  ghminv  14030  ghmmulg  14036  ghmnsgpreima  14049  ghmeqker  14051  ghmf1  14053  kerf1ghm  14054  ghmf1o  14055  gzsumsplit0  14125  gsumvalfi  14129  gsumclfi  14136  gsumsubmclfi  14140  pwssub  14193  imasring  14342  rhmopp  14456  lspcl  14700  znidomb  14965  znrrg  14967  psrbaglesuppg  14980  psrbagfi  14982  psrbaglecl  14983  psrbagcon  14985  mplsubgfilemcl  15013  iscnp4  15242  cnptopco  15246  lmtopcnp  15274  upxp  15296  uptx  15298  txlm  15303  comet  15523  metcnp3  15535  metcnp  15536  metcnp2  15537  metcnpi3  15541  elcncf2  15598  cncfco  15615  ivthreinc  15669  limcimolemlt  15688  cnplimcim  15691  cnplimclemle  15692  cnplimclemr  15693  limccnpcntop  15699  dvlemap  15704  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvef  15751  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  plycolemc  15782  plycjlemc  15784  plycj  15785  plycn  15786  plyrecj  15787  dvply1  15789  dvply2g  15790  logfac  15918  lgsval  16037  lgscllem  16040  lgsval2lem  16043  lgsval4a  16055  lgsneg  16057  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  lgseisenlem3  16105  lgseisenlem4  16106  p1evtxdeqfi  16467  wlkvtxm  16495  wlkvtxiedg  16500  wlkvtxiedgg  16501  upgriswlkdc  16515  trlsegvdeglem7  16621  trlsegvdegfi  16622  eupth2lem3lem1fi  16623  eupth2lem3lem2fi  16624  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  eupth2lem3lem7fi  16629  eupth2lemsfi  16633  3dom  16932  pwle2  16942  subctctexmid  16944  nnsf  16953  peano4nninf  16954  nninfalllem1  16956  nninfsellemdc  16958  nninfsellemeq  16962  nninfsellemqall  16963  nninfsellemeqinf  16964  nninfomnilem  16966  nnnninfex  16970  nninfnfiinf  16971  repiecelem  16979  repiecele0  16980  repiecege0  16981  isomninnlem  16984  trilpolemeq1  16994  trilpolemlt1  16995  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007  nconstwlpolemgt0  17019  nconstwlpolem  17020