Theorem ffvelcdmd 5813

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

Syntax hints:   -> wi 4   e. wcel 2203   -->wf 5348   ` cfv 5352

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 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-sbc 3043  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-fv 5360

This theorem is referenced by:  isotr  5989  caofinvl  6292  fvdifsuppst  6444  rdgon  6617  frecabcl  6630  1dom1el  7060  phplem4dom  7116  fidceq  7124  dif1en  7136  fin0  7142  fin0or  7143  infm  7164  en2eqpr  7167  fidcenumlemrks  7223  fidcenumlemr  7225  2omap  7269  supisoti  7301  ordiso2  7326  updjudhcoinlf  7371  updjudhcoinrg  7372  caseinl  7382  caseinr  7383  difinfsnlem  7390  difinfsn  7391  ctmlemr  7399  ctssdclemn0  7401  ctssdc  7404  enumctlemm  7405  enumct  7406  nnnninfeq2  7420  nninfisol  7424  enomnilem  7429  finomni  7431  ismkvnex  7446  enmkvlem  7452  enwomnilem  7460  nninfwlpoimlemg  7466  nninfwlpoimlemginf  7467  pr2cv1  7492  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  acnccim  7586  cauappcvgprlemm  7960  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdfu  7969  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlem2  7975  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemloc  7990  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem1  7994  caucvgprlem2  7995  caucvgprprlemnkltj  8004  caucvgprprlemnkeqj  8005  caucvgprprlemnbj  8008  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemloc  8018  caucvgprprlemexbt  8021  caucvgprprlemexb  8022  caucvgprprlemaddq  8023  caucvgprprlem1  8024  caucvgprprlem2  8025  caucvgsrlemcau  8108  caucvgsrlemgt1  8110  caucvgsrlemoffcau  8113  caucvgsrlemoffres  8115  caucvgsr  8117  axcaucvglemval  8212  axcaucvglemcau  8213  axcaucvglemres  8214  fseq1p1m1  10428  4fvwrd4  10474  fvinim0ffz  10587  frecuzrdgg  10778  frecuzrdgsuctlem  10785  seq3val  10822  seqvalcd  10823  seq3p1  10827  seqp1cd  10832  ser3mono  10849  seq3split  10850  seq3caopr2  10855  iseqf1olemkle  10859  iseqf1olemklt  10860  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemmo  10867  iseqf1olemqk  10869  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  seq3f1olemstep  10876  seq3f1oleml  10878  seq3f1o  10879  seqf1oglem2a  10880  seqf1oglem1  10881  seqf1oglem2  10882  seq3z  10890  seq3distr  10894  ser3ge0  10898  ser3le  10899  exp3vallem  10902  exp3val  10903  bcval5  11125  hashfz1  11146  resunimafz0  11198  leisorel  11209  zfz1isolemiso  11211  seq3coll  11214  ccatcl  11281  swrdclg  11342  caucvgrelemcau  11665  caucvgre  11666  cvg1nlemf  11668  cvg1nlemcau  11669  cvg1nlemres  11670  recvguniqlem  11679  resqrexlemdecn  11697  resqrexlemcalc3  11701  resqrexlemnmsq  11702  resqrexlemnm  11703  resqrexlemcvg  11704  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemga  11708  clim2ser  12022  clim2ser2  12023  climrecvg1n  12033  climcvg1nlem  12034  serf0  12037  sumeq2  12044  fsum3cvg  12064  summodclem2a  12067  fsum3  12073  fisumss  12078  fsumcl2lem  12084  fsumadd  12092  fsummulc2  12134  fsumrelem  12157  isumshft  12176  cvgratnnlemseq  12212  cvgratnnlemrate  12216  clim2prod  12225  clim2divap  12226  prodfrecap  12232  prodfdivap  12233  ntrivcvgap  12234  prodeq2  12243  fproddccvg  12258  prodmodclem3  12261  prodmodclem2a  12262  fprodseq  12269  fprodssdc  12276  fprodmul  12277  effsumlt  12378  nninfctlemfo  12736  nn0seqcvgd  12738  ialgrlem1st  12739  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  pcmpt2  13042  pcmptdvds  13043  1arithlem4  13064  1arith  13065  ennnfonelemdc  13150  ennnfonelemjn  13153  ennnfonelemg  13154  ennnfonelemp1  13157  ennnfonelemom  13159  ennnfonelemhdmp1  13160  ennnfonelemss  13161  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemnn0  13173  ennnfonelemim  13175  ctinfomlemom  13178  ctiunctlemudc  13188  ctiunctlemf  13189  ctiunctlemfo  13190  ssnnctlemct  13197  nninfdclemp1  13201  nninfdclemlt  13202  imasmnd2  13665  mhmf1o  13683  mhmco  13703  gsumfzcl  13712  isgrpinv  13767  pwssub  13826  imasgrp2  13827  mhmid  13832  mhmmnd  13833  ghmgrp  13835  mulgval  13839  mulgfng  13841  mulgnnsubcl  13851  ghmid  13966  ghminv  13967  ghmmulg  13973  ghmnsgpreima  13986  ghmeqker  13988  ghmf1  13990  kerf1ghm  13991  ghmf1o  13992  gsumsplit0  14063  imasring  14208  rhmopp  14321  lspcl  14539  znidomb  14806  znrrg  14808  psrbaglesuppg  14821  psrbagfi  14823  psrbaglecl  14824  psrbagcon  14826  mplsubgfilemcl  14854  iscnp4  15083  cnptopco  15087  lmtopcnp  15115  upxp  15137  uptx  15139  txlm  15144  comet  15364  metcnp3  15376  metcnp  15377  metcnp2  15378  metcnpi3  15382  elcncf2  15439  cncfco  15456  ivthreinc  15510  limcimolemlt  15529  cnplimcim  15532  cnplimclemle  15533  cnplimclemr  15534  limccnpcntop  15540  dvlemap  15545  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvef  15592  plyaddlem1  15612  plymullem1  15613  plycoeid3  15622  plycolemc  15623  plycjlemc  15625  plycj  15626  plycn  15627  plyrecj  15628  dvply1  15630  dvply2g  15631  lgsval  15877  lgscllem  15880  lgsval2lem  15883  lgsval4a  15895  lgsneg  15897  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  lgseisenlem3  15945  lgseisenlem4  15946  p1evtxdeqfi  16307  wlkvtxm  16335  wlkvtxiedg  16340  wlkvtxiedgg  16341  upgriswlkdc  16355  trlsegvdeglem7  16461  trlsegvdegfi  16462  eupth2lem3lem1fi  16463  eupth2lem3lem2fi  16464  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  eupth2lem3lem7fi  16469  eupth2lemsfi  16473  3dom  16762  pwle2  16772  subctctexmid  16774  nnsf  16783  peano4nninf  16784  nninfalllem1  16786  nninfsellemdc  16788  nninfsellemeq  16792  nninfsellemqall  16793  nninfsellemeqinf  16794  nninfomnilem  16796  nnnninfex  16800  nninfnfiinf  16801  repiecelem  16809  repiecele0  16810  repiecege0  16811  isomninnlem  16814  trilpolemeq1  16824  trilpolemlt1  16825  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837  nconstwlpolemgt0  16850  nconstwlpolem  16851  gfsumval  16862  gfsumcl  16870