Theorem ffvelcdmd 5791

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 5790	. 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 5329   ` cfv 5333

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-fv 5341

This theorem is referenced by:  isotr  5967  caofinvl  6270  fvdifsuppst  6422  rdgon  6595  frecabcl  6608  1dom1el  7036  phplem4dom  7091  fidceq  7099  dif1en  7111  fin0  7117  fin0or  7118  infm  7139  en2eqpr  7142  fidcenumlemrks  7195  fidcenumlemr  7197  supisoti  7252  ordiso2  7277  updjudhcoinlf  7322  updjudhcoinrg  7323  caseinl  7333  caseinr  7334  difinfsnlem  7341  difinfsn  7342  ctmlemr  7350  ctssdclemn0  7352  ctssdc  7355  enumctlemm  7356  enumct  7357  nnnninfeq2  7371  nninfisol  7375  enomnilem  7380  finomni  7382  ismkvnex  7397  enmkvlem  7403  enwomnilem  7411  nninfwlpoimlemg  7417  nninfwlpoimlemginf  7418  pr2cv1  7443  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  acnccim  7534  cauappcvgprlemm  7908  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdfu  7917  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlem2  7923  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemloc  7938  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem1  7942  caucvgprlem2  7943  caucvgprprlemnkltj  7952  caucvgprprlemnkeqj  7953  caucvgprprlemnbj  7956  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  caucvgprprlemexb  7970  caucvgprprlemaddq  7971  caucvgprprlem1  7972  caucvgprprlem2  7973  caucvgsrlemcau  8056  caucvgsrlemgt1  8058  caucvgsrlemoffcau  8061  caucvgsrlemoffres  8063  caucvgsr  8065  axcaucvglemval  8160  axcaucvglemcau  8161  axcaucvglemres  8162  fseq1p1m1  10374  4fvwrd4  10420  fvinim0ffz  10533  frecuzrdgg  10724  frecuzrdgsuctlem  10731  seq3val  10768  seqvalcd  10769  seq3p1  10773  seqp1cd  10778  ser3mono  10795  seq3split  10796  seq3caopr2  10801  iseqf1olemkle  10805  iseqf1olemklt  10806  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemmo  10813  iseqf1olemqk  10815  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  iseqf1olemfvp  10818  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seq3f1olemqsum  10821  seq3f1olemstep  10822  seq3f1oleml  10824  seq3f1o  10825  seqf1oglem2a  10826  seqf1oglem1  10827  seqf1oglem2  10828  seq3z  10836  seq3distr  10840  ser3ge0  10844  ser3le  10845  exp3vallem  10848  exp3val  10849  bcval5  11071  hashfz1  11091  resunimafz0  11141  leisorel  11147  zfz1isolemiso  11149  seq3coll  11152  ccatcl  11219  swrdclg  11280  caucvgrelemcau  11603  caucvgre  11604  cvg1nlemf  11606  cvg1nlemcau  11607  cvg1nlemres  11608  recvguniqlem  11617  resqrexlemdecn  11635  resqrexlemcalc3  11639  resqrexlemnmsq  11640  resqrexlemnm  11641  resqrexlemcvg  11642  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemga  11646  clim2ser  11960  clim2ser2  11961  climrecvg1n  11971  climcvg1nlem  11972  serf0  11975  sumeq2  11982  fsum3cvg  12002  summodclem2a  12005  fsum3  12011  fisumss  12016  fsumcl2lem  12022  fsumadd  12030  fsummulc2  12072  fsumrelem  12095  isumshft  12114  cvgratnnlemseq  12150  cvgratnnlemrate  12154  clim2prod  12163  clim2divap  12164  prodfrecap  12170  prodfdivap  12171  ntrivcvgap  12172  prodeq2  12181  fproddccvg  12196  prodmodclem3  12199  prodmodclem2a  12200  fprodseq  12207  fprodssdc  12214  fprodmul  12215  effsumlt  12316  nninfctlemfo  12674  nn0seqcvgd  12676  ialgrlem1st  12677  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  pcmpt2  12980  pcmptdvds  12981  1arithlem4  13002  1arith  13003  ennnfonelemdc  13083  ennnfonelemjn  13086  ennnfonelemg  13087  ennnfonelemp1  13090  ennnfonelemom  13092  ennnfonelemhdmp1  13093  ennnfonelemss  13094  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemnn0  13106  ennnfonelemim  13108  ctinfomlemom  13111  ctiunctlemudc  13121  ctiunctlemf  13122  ctiunctlemfo  13123  ssnnctlemct  13130  nninfdclemp1  13134  nninfdclemlt  13135  imasmnd2  13598  mhmf1o  13616  mhmco  13636  gsumfzcl  13645  isgrpinv  13700  pwssub  13759  imasgrp2  13760  mhmid  13765  mhmmnd  13766  ghmgrp  13768  mulgval  13772  mulgfng  13774  mulgnnsubcl  13784  ghmid  13899  ghminv  13900  ghmmulg  13906  ghmnsgpreima  13919  ghmeqker  13921  ghmf1  13923  kerf1ghm  13924  ghmf1o  13925  gsumsplit0  13996  imasring  14141  rhmopp  14254  lspcl  14470  znidomb  14737  znrrg  14739  psrbaglesuppg  14751  psrbagfi  14753  psrbaglecl  14754  psrbagcon  14755  mplsubgfilemcl  14783  iscnp4  15012  cnptopco  15016  lmtopcnp  15044  upxp  15066  uptx  15068  txlm  15073  comet  15293  metcnp3  15305  metcnp  15306  metcnp2  15307  metcnpi3  15311  elcncf2  15368  cncfco  15385  ivthreinc  15439  limcimolemlt  15458  cnplimcim  15461  cnplimclemle  15462  cnplimclemr  15463  limccnpcntop  15469  dvlemap  15474  dvcnp2cntop  15493  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  dvef  15521  plyaddlem1  15541  plymullem1  15542  plycoeid3  15551  plycolemc  15552  plycjlemc  15554  plycj  15555  plycn  15556  plyrecj  15557  dvply1  15559  dvply2g  15560  lgsval  15806  lgscllem  15809  lgsval2lem  15812  lgsval4a  15824  lgsneg  15826  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  lgseisenlem3  15874  lgseisenlem4  15875  p1evtxdeqfi  16236  wlkvtxm  16264  wlkvtxiedg  16269  wlkvtxiedgg  16270  upgriswlkdc  16284  trlsegvdeglem7  16390  trlsegvdegfi  16391  eupth2lem3lem1fi  16392  eupth2lem3lem2fi  16393  eupth2lem3lem3fi  16394  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397  eupth2lem3lem7fi  16398  eupth2lemsfi  16402  3dom  16691  2omap  16698  pwle2  16703  subctctexmid  16705  nnsf  16714  peano4nninf  16715  nninfalllem1  16717  nninfsellemdc  16719  nninfsellemeq  16723  nninfsellemqall  16724  nninfsellemeqinf  16725  nninfomnilem  16727  nnnninfex  16731  nninfnfiinf  16732  repiecelem  16740  repiecele0  16741  repiecege0  16742  isomninnlem  16745  trilpolemeq1  16755  trilpolemlt1  16756  iswomninnlem  16765  iswomni0  16767  ismkvnnlem  16768  nconstwlpolemgt0  16780  nconstwlpolem  16781  gfsumval  16792  gfsumcl  16799