Theorem ffvelcdmd 5773

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 5772	. 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 2200   -->wf 5314   ` cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-fv 5326

This theorem is referenced by:  isotr  5946  caofinvl  6250  rdgon  6538  frecabcl  6551  phplem4dom  7031  fidceq  7039  dif1en  7049  fin0  7055  fin0or  7056  infm  7077  en2eqpr  7080  fidcenumlemrks  7131  fidcenumlemr  7133  supisoti  7188  ordiso2  7213  updjudhcoinlf  7258  updjudhcoinrg  7259  caseinl  7269  caseinr  7270  difinfsnlem  7277  difinfsn  7278  ctmlemr  7286  ctssdclemn0  7288  ctssdc  7291  enumctlemm  7292  enumct  7293  nnnninfeq2  7307  nninfisol  7311  enomnilem  7316  finomni  7318  ismkvnex  7333  enmkvlem  7339  enwomnilem  7347  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  pr2cv1  7379  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acnccim  7469  cauappcvgprlemm  7843  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfu  7852  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnbj  7891  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemloc  7901  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  caucvgprprlemaddq  7906  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  caucvgsr  8000  axcaucvglemval  8095  axcaucvglemcau  8096  axcaucvglemres  8097  fseq1p1m1  10302  4fvwrd4  10348  fvinim0ffz  10459  frecuzrdgg  10650  frecuzrdgsuctlem  10657  seq3val  10694  seqvalcd  10695  seq3p1  10699  seqp1cd  10704  ser3mono  10721  seq3split  10722  seq3caopr2  10727  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemmo  10739  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1olemstep  10748  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem2a  10752  seqf1oglem1  10753  seqf1oglem2  10754  seq3z  10762  seq3distr  10766  ser3ge0  10770  ser3le  10771  exp3vallem  10774  exp3val  10775  bcval5  10997  hashfz1  11017  resunimafz0  11066  leisorel  11072  zfz1isolemiso  11074  seq3coll  11077  ccatcl  11141  swrdclg  11197  caucvgrelemcau  11506  caucvgre  11507  cvg1nlemf  11509  cvg1nlemcau  11510  cvg1nlemres  11511  recvguniqlem  11520  resqrexlemdecn  11538  resqrexlemcalc3  11542  resqrexlemnmsq  11543  resqrexlemnm  11544  resqrexlemcvg  11545  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemga  11549  clim2ser  11863  clim2ser2  11864  climrecvg1n  11874  climcvg1nlem  11875  serf0  11878  sumeq2  11885  fsum3cvg  11904  summodclem2a  11907  fsum3  11913  fisumss  11918  fsumcl2lem  11924  fsumadd  11932  fsummulc2  11974  fsumrelem  11997  isumshft  12016  cvgratnnlemseq  12052  cvgratnnlemrate  12056  clim2prod  12065  clim2divap  12066  prodfrecap  12072  prodfdivap  12073  ntrivcvgap  12074  prodeq2  12083  fproddccvg  12098  prodmodclem3  12101  prodmodclem2a  12102  fprodseq  12109  fprodssdc  12116  fprodmul  12117  effsumlt  12218  nninfctlemfo  12576  nn0seqcvgd  12578  ialgrlem1st  12579  eulerthlemrprm  12766  eulerthlema  12767  eulerthlemh  12768  pcmpt2  12882  pcmptdvds  12883  1arithlem4  12904  1arith  12905  ennnfonelemdc  12985  ennnfonelemjn  12988  ennnfonelemg  12989  ennnfonelemp1  12992  ennnfonelemom  12994  ennnfonelemhdmp1  12995  ennnfonelemss  12996  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemex  13000  ennnfonelemhom  13001  ennnfonelemnn0  13008  ennnfonelemim  13010  ctinfomlemom  13013  ctiunctlemudc  13023  ctiunctlemf  13024  ctiunctlemfo  13025  ssnnctlemct  13032  nninfdclemp1  13036  nninfdclemlt  13037  imasmnd2  13500  mhmf1o  13518  mhmco  13538  gsumfzcl  13547  isgrpinv  13602  pwssub  13661  imasgrp2  13662  mhmid  13667  mhmmnd  13668  ghmgrp  13670  mulgval  13674  mulgfng  13676  mulgnnsubcl  13686  ghmid  13801  ghminv  13802  ghmmulg  13808  ghmnsgpreima  13821  ghmeqker  13823  ghmf1  13825  kerf1ghm  13826  ghmf1o  13827  imasring  14042  rhmopp  14155  lspcl  14370  znidomb  14637  znrrg  14639  psrbaglesuppg  14651  psrbagfi  14652  mplsubgfilemcl  14678  iscnp4  14907  cnptopco  14911  lmtopcnp  14939  upxp  14961  uptx  14963  txlm  14968  comet  15188  metcnp3  15200  metcnp  15201  metcnp2  15202  metcnpi3  15206  elcncf2  15263  cncfco  15280  ivthreinc  15334  limcimolemlt  15353  cnplimcim  15356  cnplimclemle  15357  cnplimclemr  15358  limccnpcntop  15364  dvlemap  15369  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcjbr  15397  dvef  15416  plyaddlem1  15436  plymullem1  15437  plycoeid3  15446  plycolemc  15447  plycjlemc  15449  plycj  15450  plycn  15451  plyrecj  15452  dvply1  15454  dvply2g  15455  lgsval  15698  lgscllem  15701  lgsval2lem  15704  lgsval4a  15716  lgsneg  15718  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  lgseisenlem3  15766  lgseisenlem4  15767  wlkvtxm  16081  wlkvtxiedg  16086  wlkvtxiedgg  16087  upgriswlkdc  16101  1dom1el  16409  3dom  16411  2omap  16418  pwle2  16423  subctctexmid  16425  nnsf  16431  peano4nninf  16432  nninfalllem1  16434  nninfsellemdc  16436  nninfsellemeq  16440  nninfsellemqall  16441  nninfsellemeqinf  16442  nninfomnilem  16444  nnnninfex  16448  nninfnfiinf  16449  isomninnlem  16458  trilpolemeq1  16468  trilpolemlt1  16469  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480  nconstwlpolemgt0  16492  nconstwlpolem  16493