Theorem ffvelcdmd 5779

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 5778	. 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 5320   ` cfv 5324

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 4205  ax-pow 4262  ax-pr 4297

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 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-fv 5332

This theorem is referenced by:  isotr  5952  caofinvl  6256  rdgon  6547  frecabcl  6560  1dom1el  6988  phplem4dom  7043  fidceq  7051  dif1en  7061  fin0  7067  fin0or  7068  infm  7089  en2eqpr  7092  fidcenumlemrks  7143  fidcenumlemr  7145  supisoti  7200  ordiso2  7225  updjudhcoinlf  7270  updjudhcoinrg  7271  caseinl  7281  caseinr  7282  difinfsnlem  7289  difinfsn  7290  ctmlemr  7298  ctssdclemn0  7300  ctssdc  7303  enumctlemm  7304  enumct  7305  nnnninfeq2  7319  nninfisol  7323  enomnilem  7328  finomni  7330  ismkvnex  7345  enmkvlem  7351  enwomnilem  7359  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  pr2cv1  7391  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  acnccim  7481  cauappcvgprlemm  7855  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfu  7864  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlem2  7870  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgprlem2  7890  caucvgprprlemnkltj  7899  caucvgprprlemnkeqj  7900  caucvgprprlemnbj  7903  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemloc  7913  caucvgprprlemexbt  7916  caucvgprprlemexb  7917  caucvgprprlemaddq  7918  caucvgprprlem1  7919  caucvgprprlem2  7920  caucvgsrlemcau  8003  caucvgsrlemgt1  8005  caucvgsrlemoffcau  8008  caucvgsrlemoffres  8010  caucvgsr  8012  axcaucvglemval  8107  axcaucvglemcau  8108  axcaucvglemres  8109  fseq1p1m1  10319  4fvwrd4  10365  fvinim0ffz  10477  frecuzrdgg  10668  frecuzrdgsuctlem  10675  seq3val  10712  seqvalcd  10713  seq3p1  10717  seqp1cd  10722  ser3mono  10739  seq3split  10740  seq3caopr2  10745  iseqf1olemkle  10749  iseqf1olemklt  10750  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemmo  10757  iseqf1olemqk  10759  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  iseqf1olemfvp  10762  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seq3f1olemstep  10766  seq3f1oleml  10768  seq3f1o  10769  seqf1oglem2a  10770  seqf1oglem1  10771  seqf1oglem2  10772  seq3z  10780  seq3distr  10784  ser3ge0  10788  ser3le  10789  exp3vallem  10792  exp3val  10793  bcval5  11015  hashfz1  11035  resunimafz0  11085  leisorel  11091  zfz1isolemiso  11093  seq3coll  11096  ccatcl  11160  swrdclg  11221  caucvgrelemcau  11531  caucvgre  11532  cvg1nlemf  11534  cvg1nlemcau  11535  cvg1nlemres  11536  recvguniqlem  11545  resqrexlemdecn  11563  resqrexlemcalc3  11567  resqrexlemnmsq  11568  resqrexlemnm  11569  resqrexlemcvg  11570  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemga  11574  clim2ser  11888  clim2ser2  11889  climrecvg1n  11899  climcvg1nlem  11900  serf0  11903  sumeq2  11910  fsum3cvg  11929  summodclem2a  11932  fsum3  11938  fisumss  11943  fsumcl2lem  11949  fsumadd  11957  fsummulc2  11999  fsumrelem  12022  isumshft  12041  cvgratnnlemseq  12077  cvgratnnlemrate  12081  clim2prod  12090  clim2divap  12091  prodfrecap  12097  prodfdivap  12098  ntrivcvgap  12099  prodeq2  12108  fproddccvg  12123  prodmodclem3  12126  prodmodclem2a  12127  fprodseq  12134  fprodssdc  12141  fprodmul  12142  effsumlt  12243  nninfctlemfo  12601  nn0seqcvgd  12603  ialgrlem1st  12604  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemh  12793  pcmpt2  12907  pcmptdvds  12908  1arithlem4  12929  1arith  12930  ennnfonelemdc  13010  ennnfonelemjn  13013  ennnfonelemg  13014  ennnfonelemp1  13017  ennnfonelemom  13019  ennnfonelemhdmp1  13020  ennnfonelemss  13021  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemnn0  13033  ennnfonelemim  13035  ctinfomlemom  13038  ctiunctlemudc  13048  ctiunctlemf  13049  ctiunctlemfo  13050  ssnnctlemct  13057  nninfdclemp1  13061  nninfdclemlt  13062  imasmnd2  13525  mhmf1o  13543  mhmco  13563  gsumfzcl  13572  isgrpinv  13627  pwssub  13686  imasgrp2  13687  mhmid  13692  mhmmnd  13693  ghmgrp  13695  mulgval  13699  mulgfng  13701  mulgnnsubcl  13711  ghmid  13826  ghminv  13827  ghmmulg  13833  ghmnsgpreima  13846  ghmeqker  13848  ghmf1  13850  kerf1ghm  13851  ghmf1o  13852  imasring  14067  rhmopp  14180  lspcl  14395  znidomb  14662  znrrg  14664  psrbaglesuppg  14676  psrbagfi  14677  mplsubgfilemcl  14703  iscnp4  14932  cnptopco  14936  lmtopcnp  14964  upxp  14986  uptx  14988  txlm  14993  comet  15213  metcnp3  15225  metcnp  15226  metcnp2  15227  metcnpi3  15231  elcncf2  15288  cncfco  15305  ivthreinc  15359  limcimolemlt  15378  cnplimcim  15381  cnplimclemle  15382  cnplimclemr  15383  limccnpcntop  15389  dvlemap  15394  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvef  15441  plyaddlem1  15461  plymullem1  15462  plycoeid3  15471  plycolemc  15472  plycjlemc  15474  plycj  15475  plycn  15476  plyrecj  15477  dvply1  15479  dvply2g  15480  lgsval  15723  lgscllem  15726  lgsval2lem  15729  lgsval4a  15741  lgsneg  15743  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgseisenlem3  15791  lgseisenlem4  15792  wlkvtxm  16137  wlkvtxiedg  16142  wlkvtxiedgg  16143  upgriswlkdc  16157  3dom  16523  2omap  16530  pwle2  16535  subctctexmid  16537  nnsf  16543  peano4nninf  16544  nninfalllem1  16546  nninfsellemdc  16548  nninfsellemeq  16552  nninfsellemqall  16553  nninfsellemeqinf  16554  nninfomnilem  16556  nnnninfex  16560  nninfnfiinf  16561  isomninnlem  16570  trilpolemeq1  16580  trilpolemlt1  16581  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592  nconstwlpolemgt0  16604  nconstwlpolem  16605