Theorem ffvelcdmd 5770

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 5769	. 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 5313   ` cfv 5317

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 4201  ax-pow 4257  ax-pr 4292

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 3888  df-br 4083  df-opab 4145  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-iota 5277  df-fun 5319  df-fn 5320  df-f 5321  df-fv 5325

This theorem is referenced by:  isotr  5939  caofinvl  6242  rdgon  6530  frecabcl  6543  phplem4dom  7019  fidceq  7027  dif1en  7037  fin0  7043  fin0or  7044  infm  7062  en2eqpr  7065  fidcenumlemrks  7116  fidcenumlemr  7118  supisoti  7173  ordiso2  7198  updjudhcoinlf  7243  updjudhcoinrg  7244  caseinl  7254  caseinr  7255  difinfsnlem  7262  difinfsn  7263  ctmlemr  7271  ctssdclemn0  7273  ctssdc  7276  enumctlemm  7277  enumct  7278  nnnninfeq2  7292  nninfisol  7296  enomnilem  7301  finomni  7303  ismkvnex  7318  enmkvlem  7324  enwomnilem  7332  nninfwlpoimlemg  7338  nninfwlpoimlemginf  7339  pr2cv1  7364  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  acnccim  7454  cauappcvgprlemm  7828  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdfu  7837  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlem2  7843  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemloc  7858  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlem1  7862  caucvgprlem2  7863  caucvgprprlemnkltj  7872  caucvgprprlemnkeqj  7873  caucvgprprlemnbj  7876  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemloc  7886  caucvgprprlemexbt  7889  caucvgprprlemexb  7890  caucvgprprlemaddq  7891  caucvgprprlem1  7892  caucvgprprlem2  7893  caucvgsrlemcau  7976  caucvgsrlemgt1  7978  caucvgsrlemoffcau  7981  caucvgsrlemoffres  7983  caucvgsr  7985  axcaucvglemval  8080  axcaucvglemcau  8081  axcaucvglemres  8082  fseq1p1m1  10286  4fvwrd4  10332  fvinim0ffz  10442  frecuzrdgg  10633  frecuzrdgsuctlem  10640  seq3val  10677  seqvalcd  10678  seq3p1  10682  seqp1cd  10687  ser3mono  10704  seq3split  10705  seq3caopr2  10710  iseqf1olemkle  10714  iseqf1olemklt  10715  iseqf1olemqcl  10716  iseqf1olemnab  10718  iseqf1olemmo  10722  iseqf1olemqk  10724  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  iseqf1olemfvp  10727  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3f1olemqsum  10730  seq3f1olemstep  10731  seq3f1oleml  10733  seq3f1o  10734  seqf1oglem2a  10735  seqf1oglem1  10736  seqf1oglem2  10737  seq3z  10745  seq3distr  10749  ser3ge0  10753  ser3le  10754  exp3vallem  10757  exp3val  10758  bcval5  10980  hashfz1  11000  resunimafz0  11048  leisorel  11054  zfz1isolemiso  11056  seq3coll  11059  ccatcl  11123  swrdclg  11177  caucvgrelemcau  11486  caucvgre  11487  cvg1nlemf  11489  cvg1nlemcau  11490  cvg1nlemres  11491  recvguniqlem  11500  resqrexlemdecn  11518  resqrexlemcalc3  11522  resqrexlemnmsq  11523  resqrexlemnm  11524  resqrexlemcvg  11525  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemga  11529  clim2ser  11843  clim2ser2  11844  climrecvg1n  11854  climcvg1nlem  11855  serf0  11858  sumeq2  11865  fsum3cvg  11884  summodclem2a  11887  fsum3  11893  fisumss  11898  fsumcl2lem  11904  fsumadd  11912  fsummulc2  11954  fsumrelem  11977  isumshft  11996  cvgratnnlemseq  12032  cvgratnnlemrate  12036  clim2prod  12045  clim2divap  12046  prodfrecap  12052  prodfdivap  12053  ntrivcvgap  12054  prodeq2  12063  fproddccvg  12078  prodmodclem3  12081  prodmodclem2a  12082  fprodseq  12089  fprodssdc  12096  fprodmul  12097  effsumlt  12198  nninfctlemfo  12556  nn0seqcvgd  12558  ialgrlem1st  12559  eulerthlemrprm  12746  eulerthlema  12747  eulerthlemh  12748  pcmpt2  12862  pcmptdvds  12863  1arithlem4  12884  1arith  12885  ennnfonelemdc  12965  ennnfonelemjn  12968  ennnfonelemg  12969  ennnfonelemp1  12972  ennnfonelemom  12974  ennnfonelemhdmp1  12975  ennnfonelemss  12976  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemnn0  12988  ennnfonelemim  12990  ctinfomlemom  12993  ctiunctlemudc  13003  ctiunctlemf  13004  ctiunctlemfo  13005  ssnnctlemct  13012  nninfdclemp1  13016  nninfdclemlt  13017  imasmnd2  13480  mhmf1o  13498  mhmco  13518  gsumfzcl  13527  isgrpinv  13582  pwssub  13641  imasgrp2  13642  mhmid  13647  mhmmnd  13648  ghmgrp  13650  mulgval  13654  mulgfng  13656  mulgnnsubcl  13666  ghmid  13781  ghminv  13782  ghmmulg  13788  ghmnsgpreima  13801  ghmeqker  13803  ghmf1  13805  kerf1ghm  13806  ghmf1o  13807  imasring  14022  rhmopp  14134  lspcl  14349  znidomb  14616  znrrg  14618  psrbaglesuppg  14630  psrbagfi  14631  mplsubgfilemcl  14657  iscnp4  14886  cnptopco  14890  lmtopcnp  14918  upxp  14940  uptx  14942  txlm  14947  comet  15167  metcnp3  15179  metcnp  15180  metcnp2  15181  metcnpi3  15185  elcncf2  15242  cncfco  15259  ivthreinc  15313  limcimolemlt  15332  cnplimcim  15335  cnplimclemle  15336  cnplimclemr  15337  limccnpcntop  15343  dvlemap  15348  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcjbr  15376  dvef  15395  plyaddlem1  15415  plymullem1  15416  plycoeid3  15425  plycolemc  15426  plycjlemc  15428  plycj  15429  plycn  15430  plyrecj  15431  dvply1  15433  dvply2g  15434  lgsval  15677  lgscllem  15680  lgsval2lem  15683  lgsval4a  15695  lgsneg  15697  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  lgseisenlem3  15745  lgseisenlem4  15746  wlkvtxiedgg  16042  1dom1el  16312  2omap  16318  pwle2  16323  subctctexmid  16325  nnsf  16330  peano4nninf  16331  nninfalllem1  16333  nninfsellemdc  16335  nninfsellemeq  16339  nninfsellemqall  16340  nninfsellemeqinf  16341  nninfomnilem  16343  nnnninfex  16347  nninfnfiinf  16348  isomninnlem  16357  trilpolemeq1  16367  trilpolemlt1  16368  iswomninnlem  16376  iswomni0  16378  ismkvnnlem  16379  nconstwlpolemgt0  16391  nconstwlpolem  16392