Theorem ffvelrnd 5632

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 5631	. 2 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )
4	1, 3	mpdan 419	1 |- ( ph -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   e. wcel 2141   -->wf 5194   ` cfv 5198

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-sbc 2956  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-id 4278  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-fv 5206

This theorem is referenced by:  isotr  5795  caofinvl  6083  rdgon  6365  frecabcl  6378  phplem4dom  6840  fidceq  6847  dif1en  6857  fin0  6863  fin0or  6864  infm  6882  en2eqpr  6885  fidcenumlemrks  6930  fidcenumlemr  6932  supisoti  6987  ordiso2  7012  updjudhcoinlf  7057  updjudhcoinrg  7058  caseinl  7068  caseinr  7069  difinfsnlem  7076  difinfsn  7077  ctmlemr  7085  ctssdclemn0  7087  ctssdc  7090  enumctlemm  7091  enumct  7092  nnnninfeq2  7105  nninfisol  7109  enomnilem  7114  finomni  7116  ismkvnex  7131  enmkvlem  7137  enwomnilem  7145  nninfwlpoimlemg  7151  nninfwlpoimlemginf  7152  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  cauappcvgprlemm  7607  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlem2  7622  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgprlem2  7642  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemnbj  7655  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemloc  7665  caucvgprprlemexbt  7668  caucvgprprlemexb  7669  caucvgprprlemaddq  7670  caucvgprprlem1  7671  caucvgprprlem2  7672  caucvgsrlemcau  7755  caucvgsrlemgt1  7757  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  caucvgsr  7764  axcaucvglemval  7859  axcaucvglemcau  7860  axcaucvglemres  7861  fseq1p1m1  10050  4fvwrd4  10096  fvinim0ffz  10197  frecuzrdgg  10372  frecuzrdgsuctlem  10379  seq3val  10414  seqvalcd  10415  seq3p1  10418  seqp1cd  10422  ser3mono  10434  seq3split  10435  seq3caopr2  10438  iseqf1olemkle  10440  iseqf1olemklt  10441  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemmo  10448  iseqf1olemqk  10450  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1olemstep  10457  seq3f1oleml  10459  seq3f1o  10460  seq3z  10467  seq3distr  10469  ser3ge0  10473  ser3le  10474  exp3vallem  10477  exp3val  10478  bcval5  10697  hashfz1  10717  resunimafz0  10766  leisorel  10772  zfz1isolemiso  10774  seq3coll  10777  caucvgrelemcau  10944  caucvgre  10945  cvg1nlemf  10947  cvg1nlemcau  10948  cvg1nlemres  10949  recvguniqlem  10958  resqrexlemdecn  10976  resqrexlemcalc3  10980  resqrexlemnmsq  10981  resqrexlemnm  10982  resqrexlemcvg  10983  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemga  10987  clim2ser  11300  clim2ser2  11301  climrecvg1n  11311  climcvg1nlem  11312  serf0  11315  sumeq2  11322  fsum3cvg  11341  summodclem2a  11344  fsum3  11350  fisumss  11355  fsumcl2lem  11361  fsumadd  11369  fsummulc2  11411  fsumrelem  11434  isumshft  11453  cvgratnnlemseq  11489  cvgratnnlemrate  11493  clim2prod  11502  clim2divap  11503  prodfrecap  11509  prodfdivap  11510  ntrivcvgap  11511  prodeq2  11520  fproddccvg  11535  prodmodclem3  11538  prodmodclem2a  11539  fprodseq  11546  fprodssdc  11553  fprodmul  11554  effsumlt  11655  nn0seqcvgd  11995  ialgrlem1st  11996  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  pcmpt2  12296  pcmptdvds  12297  1arithlem4  12318  1arith  12319  ennnfonelemdc  12354  ennnfonelemjn  12357  ennnfonelemg  12358  ennnfonelemp1  12361  ennnfonelemom  12363  ennnfonelemhdmp1  12364  ennnfonelemss  12365  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemnn0  12377  ennnfonelemim  12379  ctinfomlemom  12382  ctiunctlemudc  12392  ctiunctlemf  12393  ctiunctlemfo  12394  ssnnctlemct  12401  nninfdclemp1  12405  nninfdclemlt  12406  mhmf1o  12693  mhmco  12705  isgrpinv  12756  iscnp4  13012  cnptopco  13016  lmtopcnp  13044  upxp  13066  uptx  13068  txlm  13073  comet  13293  metcnp3  13305  metcnp  13306  metcnp2  13307  metcnpi3  13311  elcncf2  13355  cncfco  13372  limcimolemlt  13427  cnplimcim  13430  cnplimclemle  13431  cnplimclemr  13432  limccnpcntop  13438  dvlemap  13443  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvef  13482  lgsval  13699  lgscllem  13702  lgsval2lem  13705  lgsval4a  13717  lgsneg  13719  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  pwle2  14031  subctctexmid  14034  nnsf  14038  peano4nninf  14039  nninfalllem1  14041  nninfsellemdc  14043  nninfsellemeq  14047  nninfsellemqall  14048  nninfsellemeqinf  14049  nninfomnilem  14051  isomninnlem  14062  trilpolemeq1  14072  trilpolemlt1  14073  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084  nconstwlpolemgt0  14095  nconstwlpolem  14096