Theorem ffvelcdmd 5668

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 5667	. 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 2160   -->wf 5227   ` cfv 5231

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-fv 5239

This theorem is referenced by:  isotr  5833  caofinvl  6123  rdgon  6405  frecabcl  6418  phplem4dom  6880  fidceq  6887  dif1en  6897  fin0  6903  fin0or  6904  infm  6922  en2eqpr  6925  fidcenumlemrks  6971  fidcenumlemr  6973  supisoti  7028  ordiso2  7053  updjudhcoinlf  7098  updjudhcoinrg  7099  caseinl  7109  caseinr  7110  difinfsnlem  7117  difinfsn  7118  ctmlemr  7126  ctssdclemn0  7128  ctssdc  7131  enumctlemm  7132  enumct  7133  nnnninfeq2  7146  nninfisol  7150  enomnilem  7155  finomni  7157  ismkvnex  7172  enmkvlem  7178  enwomnilem  7186  nninfwlpoimlemg  7192  nninfwlpoimlemginf  7193  exmidfodomrlemr  7220  exmidfodomrlemrALT  7221  cauappcvgprlemm  7663  cauappcvgprlemdisj  7669  cauappcvgprlemloc  7670  cauappcvgprlemladdfu  7672  cauappcvgprlemladdru  7674  cauappcvgprlemladdrl  7675  cauappcvgprlem1  7677  cauappcvgprlem2  7678  caucvgprlemnkj  7684  caucvgprlemnbj  7685  caucvgprlemm  7686  caucvgprlemloc  7693  caucvgprlemladdfu  7695  caucvgprlemladdrl  7696  caucvgprlem1  7697  caucvgprlem2  7698  caucvgprprlemnkltj  7707  caucvgprprlemnkeqj  7708  caucvgprprlemnbj  7711  caucvgprprlemmu  7713  caucvgprprlemopl  7715  caucvgprprlemloc  7721  caucvgprprlemexbt  7724  caucvgprprlemexb  7725  caucvgprprlemaddq  7726  caucvgprprlem1  7727  caucvgprprlem2  7728  caucvgsrlemcau  7811  caucvgsrlemgt1  7813  caucvgsrlemoffcau  7816  caucvgsrlemoffres  7818  caucvgsr  7820  axcaucvglemval  7915  axcaucvglemcau  7916  axcaucvglemres  7917  fseq1p1m1  10113  4fvwrd4  10159  fvinim0ffz  10260  frecuzrdgg  10435  frecuzrdgsuctlem  10442  seq3val  10477  seqvalcd  10478  seq3p1  10481  seqp1cd  10485  ser3mono  10497  seq3split  10498  seq3caopr2  10501  iseqf1olemkle  10503  iseqf1olemklt  10504  iseqf1olemqcl  10505  iseqf1olemnab  10507  iseqf1olemmo  10511  iseqf1olemqk  10513  iseqf1olemjpcl  10514  iseqf1olemqpcl  10515  iseqf1olemfvp  10516  seq3f1olemqsumkj  10517  seq3f1olemqsumk  10518  seq3f1olemqsum  10519  seq3f1olemstep  10520  seq3f1oleml  10522  seq3f1o  10523  seq3z  10530  seq3distr  10532  ser3ge0  10536  ser3le  10537  exp3vallem  10540  exp3val  10541  bcval5  10762  hashfz1  10782  resunimafz0  10830  leisorel  10836  zfz1isolemiso  10838  seq3coll  10841  caucvgrelemcau  11008  caucvgre  11009  cvg1nlemf  11011  cvg1nlemcau  11012  cvg1nlemres  11013  recvguniqlem  11022  resqrexlemdecn  11040  resqrexlemcalc3  11044  resqrexlemnmsq  11045  resqrexlemnm  11046  resqrexlemcvg  11047  resqrexlemoverl  11049  resqrexlemglsq  11050  resqrexlemga  11051  clim2ser  11364  clim2ser2  11365  climrecvg1n  11375  climcvg1nlem  11376  serf0  11379  sumeq2  11386  fsum3cvg  11405  summodclem2a  11408  fsum3  11414  fisumss  11419  fsumcl2lem  11425  fsumadd  11433  fsummulc2  11475  fsumrelem  11498  isumshft  11517  cvgratnnlemseq  11553  cvgratnnlemrate  11557  clim2prod  11566  clim2divap  11567  prodfrecap  11573  prodfdivap  11574  ntrivcvgap  11575  prodeq2  11584  fproddccvg  11599  prodmodclem3  11602  prodmodclem2a  11603  fprodseq  11610  fprodssdc  11617  fprodmul  11618  effsumlt  11719  nn0seqcvgd  12060  ialgrlem1st  12061  eulerthlemrprm  12248  eulerthlema  12249  eulerthlemh  12250  pcmpt2  12361  pcmptdvds  12362  1arithlem4  12383  1arith  12384  ennnfonelemdc  12424  ennnfonelemjn  12427  ennnfonelemg  12428  ennnfonelemp1  12431  ennnfonelemom  12433  ennnfonelemhdmp1  12434  ennnfonelemss  12435  ennnfonelemkh  12437  ennnfonelemhf1o  12438  ennnfonelemex  12439  ennnfonelemhom  12440  ennnfonelemnn0  12447  ennnfonelemim  12449  ctinfomlemom  12452  ctiunctlemudc  12462  ctiunctlemf  12463  ctiunctlemfo  12464  ssnnctlemct  12471  nninfdclemp1  12475  nninfdclemlt  12476  mhmf1o  12894  mhmco  12914  isgrpinv  12970  imasgrp2  13024  mhmid  13029  mhmmnd  13030  ghmgrp  13032  mulgval  13036  mulgfng  13038  mulgnnsubcl  13046  ghmid  13155  ghminv  13156  ghmmulg  13162  ghmnsgpreima  13175  ghmeqker  13177  ghmf1  13179  kerf1ghm  13180  ghmf1o  13181  imasring  13381  rhmopp  13493  lspcl  13674  iscnp4  14121  cnptopco  14125  lmtopcnp  14153  upxp  14175  uptx  14177  txlm  14182  comet  14402  metcnp3  14414  metcnp  14415  metcnp2  14416  metcnpi3  14420  elcncf2  14464  cncfco  14481  limcimolemlt  14536  cnplimcim  14539  cnplimclemle  14540  cnplimclemr  14541  limccnpcntop  14547  dvlemap  14552  dvcnp2cntop  14566  dvaddxxbr  14568  dvmulxxbr  14569  dvcoapbr  14574  dvcjbr  14575  dvef  14591  lgsval  14808  lgscllem  14811  lgsval2lem  14814  lgsval4a  14826  lgsneg  14828  lgsdir  14839  lgsdilem2  14840  lgsdi  14841  lgsne0  14842  1dom1el  15146  pwle2  15152  subctctexmid  15154  nnsf  15158  peano4nninf  15159  nninfalllem1  15161  nninfsellemdc  15163  nninfsellemeq  15167  nninfsellemqall  15168  nninfsellemeqinf  15169  nninfomnilem  15171  isomninnlem  15182  trilpolemeq1  15192  trilpolemlt1  15193  iswomninnlem  15201  iswomni0  15203  ismkvnnlem  15204  nconstwlpolemgt0  15216  nconstwlpolem  15217