Theorem ffvelcdmd 5734

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 5733	. 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 2177   -->wf 5281   ` cfv 5285

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4173  ax-pow 4229  ax-pr 4264

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-sbc 3003  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-br 4055  df-opab 4117  df-id 4353  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-iota 5246  df-fun 5287  df-fn 5288  df-f 5289  df-fv 5293

This theorem is referenced by:  isotr  5903  caofinvl  6202  rdgon  6490  frecabcl  6503  phplem4dom  6979  fidceq  6987  dif1en  6997  fin0  7003  fin0or  7004  infm  7022  en2eqpr  7025  fidcenumlemrks  7076  fidcenumlemr  7078  supisoti  7133  ordiso2  7158  updjudhcoinlf  7203  updjudhcoinrg  7204  caseinl  7214  caseinr  7215  difinfsnlem  7222  difinfsn  7223  ctmlemr  7231  ctssdclemn0  7233  ctssdc  7236  enumctlemm  7237  enumct  7238  nnnninfeq2  7252  nninfisol  7256  enomnilem  7261  finomni  7263  ismkvnex  7278  enmkvlem  7284  enwomnilem  7292  nninfwlpoimlemg  7298  nninfwlpoimlemginf  7299  pr2cv1  7324  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  acnccim  7414  cauappcvgprlemm  7788  cauappcvgprlemdisj  7794  cauappcvgprlemloc  7795  cauappcvgprlemladdfu  7797  cauappcvgprlemladdru  7799  cauappcvgprlemladdrl  7800  cauappcvgprlem1  7802  cauappcvgprlem2  7803  caucvgprlemnkj  7809  caucvgprlemnbj  7810  caucvgprlemm  7811  caucvgprlemloc  7818  caucvgprlemladdfu  7820  caucvgprlemladdrl  7821  caucvgprlem1  7822  caucvgprlem2  7823  caucvgprprlemnkltj  7832  caucvgprprlemnkeqj  7833  caucvgprprlemnbj  7836  caucvgprprlemmu  7838  caucvgprprlemopl  7840  caucvgprprlemloc  7846  caucvgprprlemexbt  7849  caucvgprprlemexb  7850  caucvgprprlemaddq  7851  caucvgprprlem1  7852  caucvgprprlem2  7853  caucvgsrlemcau  7936  caucvgsrlemgt1  7938  caucvgsrlemoffcau  7941  caucvgsrlemoffres  7943  caucvgsr  7945  axcaucvglemval  8040  axcaucvglemcau  8041  axcaucvglemres  8042  fseq1p1m1  10246  4fvwrd4  10292  fvinim0ffz  10402  frecuzrdgg  10593  frecuzrdgsuctlem  10600  seq3val  10637  seqvalcd  10638  seq3p1  10642  seqp1cd  10647  ser3mono  10664  seq3split  10665  seq3caopr2  10670  iseqf1olemkle  10674  iseqf1olemklt  10675  iseqf1olemqcl  10676  iseqf1olemnab  10678  iseqf1olemmo  10682  iseqf1olemqk  10684  iseqf1olemjpcl  10685  iseqf1olemqpcl  10686  iseqf1olemfvp  10687  seq3f1olemqsumkj  10688  seq3f1olemqsumk  10689  seq3f1olemqsum  10690  seq3f1olemstep  10691  seq3f1oleml  10693  seq3f1o  10694  seqf1oglem2a  10695  seqf1oglem1  10696  seqf1oglem2  10697  seq3z  10705  seq3distr  10709  ser3ge0  10713  ser3le  10714  exp3vallem  10717  exp3val  10718  bcval5  10940  hashfz1  10960  resunimafz0  11008  leisorel  11014  zfz1isolemiso  11016  seq3coll  11019  ccatcl  11082  swrdclg  11136  caucvgrelemcau  11376  caucvgre  11377  cvg1nlemf  11379  cvg1nlemcau  11380  cvg1nlemres  11381  recvguniqlem  11390  resqrexlemdecn  11408  resqrexlemcalc3  11412  resqrexlemnmsq  11413  resqrexlemnm  11414  resqrexlemcvg  11415  resqrexlemoverl  11417  resqrexlemglsq  11418  resqrexlemga  11419  clim2ser  11733  clim2ser2  11734  climrecvg1n  11744  climcvg1nlem  11745  serf0  11748  sumeq2  11755  fsum3cvg  11774  summodclem2a  11777  fsum3  11783  fisumss  11788  fsumcl2lem  11794  fsumadd  11802  fsummulc2  11844  fsumrelem  11867  isumshft  11886  cvgratnnlemseq  11922  cvgratnnlemrate  11926  clim2prod  11935  clim2divap  11936  prodfrecap  11942  prodfdivap  11943  ntrivcvgap  11944  prodeq2  11953  fproddccvg  11968  prodmodclem3  11971  prodmodclem2a  11972  fprodseq  11979  fprodssdc  11986  fprodmul  11987  effsumlt  12088  nninfctlemfo  12446  nn0seqcvgd  12448  ialgrlem1st  12449  eulerthlemrprm  12636  eulerthlema  12637  eulerthlemh  12638  pcmpt2  12752  pcmptdvds  12753  1arithlem4  12774  1arith  12775  ennnfonelemdc  12855  ennnfonelemjn  12858  ennnfonelemg  12859  ennnfonelemp1  12862  ennnfonelemom  12864  ennnfonelemhdmp1  12865  ennnfonelemss  12866  ennnfonelemkh  12868  ennnfonelemhf1o  12869  ennnfonelemex  12870  ennnfonelemhom  12871  ennnfonelemnn0  12878  ennnfonelemim  12880  ctinfomlemom  12883  ctiunctlemudc  12893  ctiunctlemf  12894  ctiunctlemfo  12895  ssnnctlemct  12902  nninfdclemp1  12906  nninfdclemlt  12907  imasmnd2  13369  mhmf1o  13387  mhmco  13407  gsumfzcl  13416  isgrpinv  13471  pwssub  13530  imasgrp2  13531  mhmid  13536  mhmmnd  13537  ghmgrp  13539  mulgval  13543  mulgfng  13545  mulgnnsubcl  13555  ghmid  13670  ghminv  13671  ghmmulg  13677  ghmnsgpreima  13690  ghmeqker  13692  ghmf1  13694  kerf1ghm  13695  ghmf1o  13696  imasring  13911  rhmopp  14023  lspcl  14238  znidomb  14505  znrrg  14507  psrbaglesuppg  14519  psrbagfi  14520  mplsubgfilemcl  14546  iscnp4  14775  cnptopco  14779  lmtopcnp  14807  upxp  14829  uptx  14831  txlm  14836  comet  15056  metcnp3  15068  metcnp  15069  metcnp2  15070  metcnpi3  15074  elcncf2  15131  cncfco  15148  ivthreinc  15202  limcimolemlt  15221  cnplimcim  15224  cnplimclemle  15225  cnplimclemr  15226  limccnpcntop  15232  dvlemap  15237  dvcnp2cntop  15256  dvaddxxbr  15258  dvmulxxbr  15259  dvcoapbr  15264  dvcjbr  15265  dvef  15284  plyaddlem1  15304  plymullem1  15305  plycoeid3  15314  plycolemc  15315  plycjlemc  15317  plycj  15318  plycn  15319  plyrecj  15320  dvply1  15322  dvply2g  15323  lgsval  15566  lgscllem  15569  lgsval2lem  15572  lgsval4a  15584  lgsneg  15586  lgsdir  15597  lgsdilem2  15598  lgsdi  15599  lgsne0  15600  lgseisenlem3  15634  lgseisenlem4  15635  1dom1el  16096  2omap  16102  pwle2  16107  subctctexmid  16109  nnsf  16114  peano4nninf  16115  nninfalllem1  16117  nninfsellemdc  16119  nninfsellemeq  16123  nninfsellemqall  16124  nninfsellemeqinf  16125  nninfomnilem  16127  nnnninfex  16131  nninfnfiinf  16132  isomninnlem  16141  trilpolemeq1  16151  trilpolemlt1  16152  iswomninnlem  16160  iswomni0  16162  ismkvnnlem  16163  nconstwlpolemgt0  16175  nconstwlpolem  16176