Theorem ffvelrnd 5620

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 5619	. 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 2136   -->wf 5183   ` cfv 5187

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4099  ax-pow 4152  ax-pr 4186

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-rex 2449  df-v 2727  df-sbc 2951  df-un 3119  df-in 3121  df-ss 3128  df-pw 3560  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-opab 4043  df-id 4270  df-xp 4609  df-rel 4610  df-cnv 4611  df-co 4612  df-dm 4613  df-rn 4614  df-iota 5152  df-fun 5189  df-fn 5190  df-f 5191  df-fv 5195

This theorem is referenced by:  isotr  5783  caofinvl  6071  rdgon  6350  frecabcl  6363  phplem4dom  6824  fidceq  6831  dif1en  6841  fin0  6847  fin0or  6848  infm  6866  en2eqpr  6869  fidcenumlemrks  6914  fidcenumlemr  6916  supisoti  6971  ordiso2  6996  updjudhcoinlf  7041  updjudhcoinrg  7042  caseinl  7052  caseinr  7053  difinfsnlem  7060  difinfsn  7061  ctmlemr  7069  ctssdclemn0  7071  ctssdc  7074  enumctlemm  7075  enumct  7076  nnnninfeq2  7089  nninfisol  7093  enomnilem  7098  finomni  7100  ismkvnex  7115  enmkvlem  7121  enwomnilem  7129  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  cauappcvgprlemm  7582  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlem2  7597  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgprlem2  7617  caucvgprprlemnkltj  7626  caucvgprprlemnkeqj  7627  caucvgprprlemnbj  7630  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemloc  7640  caucvgprprlemexbt  7643  caucvgprprlemexb  7644  caucvgprprlemaddq  7645  caucvgprprlem1  7646  caucvgprprlem2  7647  caucvgsrlemcau  7730  caucvgsrlemgt1  7732  caucvgsrlemoffcau  7735  caucvgsrlemoffres  7737  caucvgsr  7739  axcaucvglemval  7834  axcaucvglemcau  7835  axcaucvglemres  7836  fseq1p1m1  10025  4fvwrd4  10071  fvinim0ffz  10172  frecuzrdgg  10347  frecuzrdgsuctlem  10354  seq3val  10389  seqvalcd  10390  seq3p1  10393  seqp1cd  10397  ser3mono  10409  seq3split  10410  seq3caopr2  10413  iseqf1olemkle  10415  iseqf1olemklt  10416  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemmo  10423  iseqf1olemqk  10425  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  iseqf1olemfvp  10428  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3f1olemstep  10432  seq3f1oleml  10434  seq3f1o  10435  seq3z  10442  seq3distr  10444  ser3ge0  10448  ser3le  10449  exp3vallem  10452  exp3val  10453  bcval5  10672  hashfz1  10692  resunimafz0  10740  leisorel  10746  zfz1isolemiso  10748  seq3coll  10751  caucvgrelemcau  10918  caucvgre  10919  cvg1nlemf  10921  cvg1nlemcau  10922  cvg1nlemres  10923  recvguniqlem  10932  resqrexlemdecn  10950  resqrexlemcalc3  10954  resqrexlemnmsq  10955  resqrexlemnm  10956  resqrexlemcvg  10957  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemga  10961  clim2ser  11274  clim2ser2  11275  climrecvg1n  11285  climcvg1nlem  11286  serf0  11289  sumeq2  11296  fsum3cvg  11315  summodclem2a  11318  fsum3  11324  fisumss  11329  fsumcl2lem  11335  fsumadd  11343  fsummulc2  11385  fsumrelem  11408  isumshft  11427  cvgratnnlemseq  11463  cvgratnnlemrate  11467  clim2prod  11476  clim2divap  11477  prodfrecap  11483  prodfdivap  11484  ntrivcvgap  11485  prodeq2  11494  fproddccvg  11509  prodmodclem3  11512  prodmodclem2a  11513  fprodseq  11520  fprodssdc  11527  fprodmul  11528  effsumlt  11629  nn0seqcvgd  11969  ialgrlem1st  11970  eulerthlemrprm  12157  eulerthlema  12158  eulerthlemh  12159  pcmpt2  12270  pcmptdvds  12271  1arithlem4  12292  1arith  12293  ennnfonelemdc  12328  ennnfonelemjn  12331  ennnfonelemg  12332  ennnfonelemp1  12335  ennnfonelemom  12337  ennnfonelemhdmp1  12338  ennnfonelemss  12339  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemnn0  12351  ennnfonelemim  12353  ctinfomlemom  12356  ctiunctlemudc  12366  ctiunctlemf  12367  ctiunctlemfo  12368  ssnnctlemct  12375  nninfdclemp1  12379  nninfdclemlt  12380  iscnp4  12818  cnptopco  12822  lmtopcnp  12850  upxp  12872  uptx  12874  txlm  12879  comet  13099  metcnp3  13111  metcnp  13112  metcnp2  13113  metcnpi3  13117  elcncf2  13161  cncfco  13178  limcimolemlt  13233  cnplimcim  13236  cnplimclemle  13237  cnplimclemr  13238  limccnpcntop  13244  dvlemap  13249  dvcnp2cntop  13263  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvef  13288  lgsval  13505  lgscllem  13508  lgsval2lem  13511  lgsval4a  13523  lgsneg  13525  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  pwle2  13838  subctctexmid  13841  nnsf  13845  peano4nninf  13846  nninfalllem1  13848  nninfsellemdc  13850  nninfsellemeq  13854  nninfsellemqall  13855  nninfsellemeqinf  13856  nninfomnilem  13858  isomninnlem  13869  trilpolemeq1  13879  trilpolemlt1  13880  iswomninnlem  13888  iswomni0  13890  ismkvnnlem  13891  nconstwlpolemgt0  13902  nconstwlpolem  13903