Theorem ffvelrnd 5603

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypotheses

Ref	Expression
ffvelrnd.1	|- ( ph -> F : A --> B )
ffvelrnd.2	|- ( ph -> C e. A )

Assertion

Ref	Expression
ffvelrnd	|- ( ph -> ( F ` C ) e. B )

Proof of Theorem ffvelrnd

Step	Hyp	Ref	Expression
1		ffvelrnd.2	. 2 |- ( ph -> C e. A )
2		ffvelrnd.1	. . 3 |- ( ph -> F : A --> B )
3	2	ffvelrnda 5602	. 2 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )
4	1, 3	mpdan 418	1 |- ( ph -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   e. wcel 2128   -->wf 5166   ` cfv 5170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-sbc 2938  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-id 4253  df-xp 4592  df-rel 4593  df-cnv 4594  df-co 4595  df-dm 4596  df-rn 4597  df-iota 5135  df-fun 5172  df-fn 5173  df-f 5174  df-fv 5178

This theorem is referenced by:  isotr  5766  caofinvl  6054  rdgon  6333  frecabcl  6346  phplem4dom  6807  fidceq  6814  dif1en  6824  fin0  6830  fin0or  6831  infm  6849  en2eqpr  6852  fidcenumlemrks  6897  fidcenumlemr  6899  supisoti  6954  ordiso2  6979  updjudhcoinlf  7024  updjudhcoinrg  7025  caseinl  7035  caseinr  7036  difinfsnlem  7043  difinfsn  7044  ctmlemr  7052  ctssdclemn0  7054  ctssdc  7057  enumctlemm  7058  enumct  7059  nnnninfeq2  7072  nninfisol  7076  enomnilem  7081  finomni  7083  ismkvnex  7098  enmkvlem  7104  enwomnilem  7112  exmidfodomrlemr  7137  exmidfodomrlemrALT  7138  cauappcvgprlemm  7565  cauappcvgprlemdisj  7571  cauappcvgprlemloc  7572  cauappcvgprlemladdfu  7574  cauappcvgprlemladdru  7576  cauappcvgprlemladdrl  7577  cauappcvgprlem1  7579  cauappcvgprlem2  7580  caucvgprlemnkj  7586  caucvgprlemnbj  7587  caucvgprlemm  7588  caucvgprlemloc  7595  caucvgprlemladdfu  7597  caucvgprlemladdrl  7598  caucvgprlem1  7599  caucvgprlem2  7600  caucvgprprlemnkltj  7609  caucvgprprlemnkeqj  7610  caucvgprprlemnbj  7613  caucvgprprlemmu  7615  caucvgprprlemopl  7617  caucvgprprlemloc  7623  caucvgprprlemexbt  7626  caucvgprprlemexb  7627  caucvgprprlemaddq  7628  caucvgprprlem1  7629  caucvgprprlem2  7630  caucvgsrlemcau  7713  caucvgsrlemgt1  7715  caucvgsrlemoffcau  7718  caucvgsrlemoffres  7720  caucvgsr  7722  axcaucvglemval  7817  axcaucvglemcau  7818  axcaucvglemres  7819  fseq1p1m1  9996  4fvwrd4  10039  fvinim0ffz  10140  frecuzrdgg  10315  frecuzrdgsuctlem  10322  seq3val  10357  seqvalcd  10358  seq3p1  10361  seqp1cd  10365  ser3mono  10377  seq3split  10378  seq3caopr2  10381  iseqf1olemkle  10383  iseqf1olemklt  10384  iseqf1olemqcl  10385  iseqf1olemnab  10387  iseqf1olemmo  10391  iseqf1olemqk  10393  iseqf1olemjpcl  10394  iseqf1olemqpcl  10395  iseqf1olemfvp  10396  seq3f1olemqsumkj  10397  seq3f1olemqsumk  10398  seq3f1olemqsum  10399  seq3f1olemstep  10400  seq3f1oleml  10402  seq3f1o  10403  seq3z  10410  seq3distr  10412  ser3ge0  10416  ser3le  10417  exp3vallem  10420  exp3val  10421  bcval5  10637  hashfz1  10657  resunimafz0  10702  leisorel  10708  zfz1isolemiso  10710  seq3coll  10713  caucvgrelemcau  10880  caucvgre  10881  cvg1nlemf  10883  cvg1nlemcau  10884  cvg1nlemres  10885  recvguniqlem  10894  resqrexlemdecn  10912  resqrexlemcalc3  10916  resqrexlemnmsq  10917  resqrexlemnm  10918  resqrexlemcvg  10919  resqrexlemoverl  10921  resqrexlemglsq  10922  resqrexlemga  10923  clim2ser  11234  clim2ser2  11235  climrecvg1n  11245  climcvg1nlem  11246  serf0  11249  sumeq2  11256  fsum3cvg  11275  summodclem2a  11278  fsum3  11284  fisumss  11289  fsumcl2lem  11295  fsumadd  11303  fsummulc2  11345  fsumrelem  11368  isumshft  11387  cvgratnnlemseq  11423  cvgratnnlemrate  11427  clim2prod  11436  clim2divap  11437  prodfrecap  11443  prodfdivap  11444  ntrivcvgap  11445  prodeq2  11454  fproddccvg  11469  prodmodclem3  11472  prodmodclem2a  11473  fprodseq  11480  fprodssdc  11487  fprodmul  11488  effsumlt  11589  nn0seqcvgd  11918  ialgrlem1st  11919  eulerthlemrprm  12104  eulerthlema  12105  eulerthlemh  12106  ennnfonelemdc  12139  ennnfonelemjn  12142  ennnfonelemg  12143  ennnfonelemp1  12146  ennnfonelemom  12148  ennnfonelemhdmp1  12149  ennnfonelemss  12150  ennnfonelemkh  12152  ennnfonelemhf1o  12153  ennnfonelemex  12154  ennnfonelemhom  12155  ennnfonelemnn0  12162  ennnfonelemim  12164  ctinfomlemom  12167  ctiunctlemudc  12177  ctiunctlemf  12178  ctiunctlemfo  12179  ssnnctlemct  12186  nninfdclemp1  12192  nninfdclemlt  12193  iscnp4  12629  cnptopco  12633  lmtopcnp  12661  upxp  12683  uptx  12685  txlm  12690  comet  12910  metcnp3  12922  metcnp  12923  metcnp2  12924  metcnpi3  12928  elcncf2  12972  cncfco  12989  limcimolemlt  13044  cnplimcim  13047  cnplimclemle  13048  cnplimclemr  13049  limccnpcntop  13055  dvlemap  13060  dvcnp2cntop  13074  dvaddxxbr  13076  dvmulxxbr  13077  dvcoapbr  13082  dvcjbr  13083  dvef  13099  pwle2  13581  subctctexmid  13584  nnsf  13588  peano4nninf  13589  nninfalllem1  13591  nninfsellemdc  13593  nninfsellemeq  13597  nninfsellemqall  13598  nninfsellemeqinf  13599  nninfomnilem  13601  isomninnlem  13612  trilpolemeq1  13622  trilpolemlt1  13623  iswomninnlem  13631  iswomni0  13633  ismkvnnlem  13634  nconstwlpolemgt0  13645  nconstwlpolem  13646