Theorem ffvelcdmd 5818

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 5817	. 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 2205   -->wf 5353   ` 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-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-fv 5365

This theorem is referenced by:  isotr  5995  caofinvl  6301  fvdifsuppst  6457  rdgon  6630  frecabcl  6643  1dom1el  7073  phplem4dom  7129  fidceq  7137  dif1en  7149  fin0  7155  fin0or  7156  infm  7177  en2eqpr  7180  fidcenumlemrks  7236  fidcenumlemr  7238  2omap  7282  supisoti  7314  ordiso2  7339  updjudhcoinlf  7384  updjudhcoinrg  7385  caseinl  7395  caseinr  7396  difinfsnlem  7403  difinfsn  7404  ctmlemr  7412  ctssdclemn0  7414  ctssdc  7417  enumctlemm  7418  enumct  7419  nnnninfeq2  7433  nninfisol  7437  enomnilem  7442  finomni  7444  ismkvnex  7459  enmkvlem  7465  enwomnilem  7473  nninfwlpoimlemg  7479  nninfwlpoimlemginf  7480  pr2cv1  7505  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  acnccim  7602  cauappcvgprlemm  7976  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlem2  7991  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgprlem2  8011  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnbj  8024  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemexb  8038  caucvgprprlemaddq  8039  caucvgprprlem1  8040  caucvgprprlem2  8041  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  caucvgsr  8133  axcaucvglemval  8228  axcaucvglemcau  8229  axcaucvglemres  8230  fseq1p1m1  10450  4fvwrd4  10496  fvinim0ffz  10609  frecuzrdgg  10802  frecuzrdgsuctlem  10809  seq3val  10846  seqvalcd  10847  seq3p1  10851  seqp1cd  10856  ser3mono  10873  seq3split  10874  seq3caopr2  10879  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemmo  10891  iseqf1olemqk  10893  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  iseqf1olemfvp  10896  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1olemstep  10900  seq3f1oleml  10902  seq3f1o  10903  seqf1oglem2a  10904  seqf1oglem1  10905  seqf1oglem2  10906  seq3z  10914  seq3distr  10918  ser3ge0  10922  ser3le  10923  exp3vallem  10926  exp3val  10927  bcval5  11150  hashfz1  11171  resunimafz0  11223  leisorel  11234  zfz1isolemiso  11236  seq3coll  11239  ccatcl  11306  swrdclg  11367  caucvgrelemcau  11690  caucvgre  11691  cvg1nlemf  11693  cvg1nlemcau  11694  cvg1nlemres  11695  recvguniqlem  11704  resqrexlemdecn  11722  resqrexlemcalc3  11726  resqrexlemnmsq  11727  resqrexlemnm  11728  resqrexlemcvg  11729  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemga  11733  clim2ser  12047  clim2ser2  12048  climrecvg1n  12058  climcvg1nlem  12059  serf0  12062  sumeq2  12069  fsum3cvg  12089  summodclem2a  12092  fsum3  12098  fisumss  12103  fsumcl2lem  12109  fsumadd  12117  fsummulc2  12159  fsumrelem  12182  isumshft  12201  cvgratnnlemseq  12237  cvgratnnlemrate  12241  clim2prod  12250  clim2divap  12251  prodfrecap  12257  prodfdivap  12258  ntrivcvgap  12259  prodeq2  12268  fproddccvg  12283  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  fprodssdc  12301  fprodmul  12302  effsumlt  12403  nninfctlemfo  12761  nn0seqcvgd  12763  ialgrlem1st  12764  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  pcmpt2  13067  pcmptdvds  13068  1arithlem4  13089  1arith  13090  ennnfonelemdc  13234  ennnfonelemjn  13237  ennnfonelemg  13238  ennnfonelemp1  13241  ennnfonelemom  13243  ennnfonelemhdmp1  13244  ennnfonelemss  13245  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemnn0  13257  ennnfonelemim  13259  ctinfomlemom  13262  ctiunctlemudc  13272  ctiunctlemf  13273  ctiunctlemfo  13274  ssnnctlemct  13281  nninfdclemp1  13285  nninfdclemlt  13286  imasmnd2  13707  mhmf1o  13725  mhmco  13745  gsumfzcl  13754  isgrpinv  13809  imasgrp2  13863  mhmid  13868  mhmmnd  13869  ghmgrp  13871  mulgval  13875  mulgfng  13877  mulgnnsubcl  13887  ghmid  14002  ghminv  14003  ghmmulg  14009  ghmnsgpreima  14022  ghmeqker  14024  ghmf1  14026  kerf1ghm  14027  ghmf1o  14028  gsumsplit0  14099  gfsumval  14102  gfsumcl  14110  pwssub  14158  imasring  14307  rhmopp  14421  lspcl  14665  znidomb  14932  znrrg  14934  psrbaglesuppg  14947  psrbagfi  14949  psrbaglecl  14950  psrbagcon  14952  mplsubgfilemcl  14980  iscnp4  15209  cnptopco  15213  lmtopcnp  15241  upxp  15263  uptx  15265  txlm  15270  comet  15490  metcnp3  15502  metcnp  15503  metcnp2  15504  metcnpi3  15508  elcncf2  15565  cncfco  15582  ivthreinc  15636  limcimolemlt  15655  cnplimcim  15658  cnplimclemle  15659  cnplimclemr  15660  limccnpcntop  15666  dvlemap  15671  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvef  15718  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  plycolemc  15749  plycjlemc  15751  plycj  15752  plycn  15753  plyrecj  15754  dvply1  15756  dvply2g  15757  lgsval  16003  lgscllem  16006  lgsval2lem  16009  lgsval4a  16021  lgsneg  16023  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgseisenlem3  16071  lgseisenlem4  16072  p1evtxdeqfi  16433  wlkvtxm  16461  wlkvtxiedg  16466  wlkvtxiedgg  16467  upgriswlkdc  16481  trlsegvdeglem7  16587  trlsegvdegfi  16588  eupth2lem3lem1fi  16589  eupth2lem3lem2fi  16590  eupth2lem3lem3fi  16591  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  eupth2lem3lem7fi  16595  eupth2lemsfi  16599  3dom  16888  pwle2  16898  subctctexmid  16900  nnsf  16909  peano4nninf  16910  nninfalllem1  16912  nninfsellemdc  16914  nninfsellemeq  16918  nninfsellemqall  16919  nninfsellemeqinf  16920  nninfomnilem  16922  nnnninfex  16926  nninfnfiinf  16927  repiecelem  16935  repiecele0  16936  repiecege0  16937  isomninnlem  16940  trilpolemeq1  16950  trilpolemlt1  16951  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963  nconstwlpolemgt0  16976  nconstwlpolem  16977