Theorem ffvelcdmd 5783

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 5782	. 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 2202   -->wf 5322   ` cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334

This theorem is referenced by:  isotr  5957  caofinvl  6261  rdgon  6552  frecabcl  6565  1dom1el  6993  phplem4dom  7048  fidceq  7056  dif1en  7068  fin0  7074  fin0or  7075  infm  7096  en2eqpr  7099  fidcenumlemrks  7152  fidcenumlemr  7154  supisoti  7209  ordiso2  7234  updjudhcoinlf  7279  updjudhcoinrg  7280  caseinl  7290  caseinr  7291  difinfsnlem  7298  difinfsn  7299  ctmlemr  7307  ctssdclemn0  7309  ctssdc  7312  enumctlemm  7313  enumct  7314  nnnninfeq2  7328  nninfisol  7332  enomnilem  7337  finomni  7339  ismkvnex  7354  enmkvlem  7360  enwomnilem  7368  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  pr2cv1  7400  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acnccim  7491  cauappcvgprlemm  7865  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprlem2  7900  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnbj  7913  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  caucvgprprlemaddq  7928  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  caucvgsr  8022  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  fseq1p1m1  10329  4fvwrd4  10375  fvinim0ffz  10488  frecuzrdgg  10679  frecuzrdgsuctlem  10686  seq3val  10723  seqvalcd  10724  seq3p1  10728  seqp1cd  10733  ser3mono  10750  seq3split  10751  seq3caopr2  10756  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemmo  10768  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem2a  10781  seqf1oglem1  10782  seqf1oglem2  10783  seq3z  10791  seq3distr  10795  ser3ge0  10799  ser3le  10800  exp3vallem  10803  exp3val  10804  bcval5  11026  hashfz1  11046  resunimafz0  11096  leisorel  11102  zfz1isolemiso  11104  seq3coll  11107  ccatcl  11174  swrdclg  11235  caucvgrelemcau  11558  caucvgre  11559  cvg1nlemf  11561  cvg1nlemcau  11562  cvg1nlemres  11563  recvguniqlem  11572  resqrexlemdecn  11590  resqrexlemcalc3  11594  resqrexlemnmsq  11595  resqrexlemnm  11596  resqrexlemcvg  11597  resqrexlemoverl  11599  resqrexlemglsq  11600  resqrexlemga  11601  clim2ser  11915  clim2ser2  11916  climrecvg1n  11926  climcvg1nlem  11927  serf0  11930  sumeq2  11937  fsum3cvg  11957  summodclem2a  11960  fsum3  11966  fisumss  11971  fsumcl2lem  11977  fsumadd  11985  fsummulc2  12027  fsumrelem  12050  isumshft  12069  cvgratnnlemseq  12105  cvgratnnlemrate  12109  clim2prod  12118  clim2divap  12119  prodfrecap  12125  prodfdivap  12126  ntrivcvgap  12127  prodeq2  12136  fproddccvg  12151  prodmodclem3  12154  prodmodclem2a  12155  fprodseq  12162  fprodssdc  12169  fprodmul  12170  effsumlt  12271  nninfctlemfo  12629  nn0seqcvgd  12631  ialgrlem1st  12632  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemh  12821  pcmpt2  12935  pcmptdvds  12936  1arithlem4  12957  1arith  12958  ennnfonelemdc  13038  ennnfonelemjn  13041  ennnfonelemg  13042  ennnfonelemp1  13045  ennnfonelemom  13047  ennnfonelemhdmp1  13048  ennnfonelemss  13049  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemnn0  13061  ennnfonelemim  13063  ctinfomlemom  13066  ctiunctlemudc  13076  ctiunctlemf  13077  ctiunctlemfo  13078  ssnnctlemct  13085  nninfdclemp1  13089  nninfdclemlt  13090  imasmnd2  13553  mhmf1o  13571  mhmco  13591  gsumfzcl  13600  isgrpinv  13655  pwssub  13714  imasgrp2  13715  mhmid  13720  mhmmnd  13721  ghmgrp  13723  mulgval  13727  mulgfng  13729  mulgnnsubcl  13739  ghmid  13854  ghminv  13855  ghmmulg  13861  ghmnsgpreima  13874  ghmeqker  13876  ghmf1  13878  kerf1ghm  13879  ghmf1o  13880  gsumsplit0  13951  imasring  14096  rhmopp  14209  lspcl  14424  znidomb  14691  znrrg  14693  psrbaglesuppg  14705  psrbagfi  14706  mplsubgfilemcl  14732  iscnp4  14961  cnptopco  14965  lmtopcnp  14993  upxp  15015  uptx  15017  txlm  15022  comet  15242  metcnp3  15254  metcnp  15255  metcnp2  15256  metcnpi3  15260  elcncf2  15317  cncfco  15334  ivthreinc  15388  limcimolemlt  15407  cnplimcim  15410  cnplimclemle  15411  cnplimclemr  15412  limccnpcntop  15418  dvlemap  15423  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvef  15470  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  plycolemc  15501  plycjlemc  15503  plycj  15504  plycn  15505  plyrecj  15506  dvply1  15508  dvply2g  15509  lgsval  15752  lgscllem  15755  lgsval2lem  15758  lgsval4a  15770  lgsneg  15772  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  lgseisenlem3  15820  lgseisenlem4  15821  p1evtxdeqfi  16182  wlkvtxm  16210  wlkvtxiedg  16215  wlkvtxiedgg  16216  upgriswlkdc  16230  trlsegvdeglem7  16336  trlsegvdegfi  16337  eupth2lem3lem1fi  16338  eupth2lem3lem2fi  16339  eupth2lem3lem3fi  16340  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  eupth2lem3lem7fi  16344  eupth2lemsfi  16348  3dom  16638  2omap  16645  pwle2  16650  subctctexmid  16652  nnsf  16658  peano4nninf  16659  nninfalllem1  16661  nninfsellemdc  16663  nninfsellemeq  16667  nninfsellemqall  16668  nninfsellemeqinf  16669  nninfomnilem  16671  nnnninfex  16675  nninfnfiinf  16676  isomninnlem  16685  trilpolemeq1  16695  trilpolemlt1  16696  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708  nconstwlpolemgt0  16720  nconstwlpolem  16721  gfsumval  16732  gfsumcl  16739