Theorem ffvelcdmd 5715

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 5714	. 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 2175   -->wf 5266   ` cfv 5270

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-sbc 2998  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-id 4339  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-rn 4685  df-iota 5231  df-fun 5272  df-fn 5273  df-f 5274  df-fv 5278

This theorem is referenced by:  isotr  5884  caofinvl  6183  rdgon  6471  frecabcl  6484  phplem4dom  6958  fidceq  6965  dif1en  6975  fin0  6981  fin0or  6982  infm  7000  en2eqpr  7003  fidcenumlemrks  7054  fidcenumlemr  7056  supisoti  7111  ordiso2  7136  updjudhcoinlf  7181  updjudhcoinrg  7182  caseinl  7192  caseinr  7193  difinfsnlem  7200  difinfsn  7201  ctmlemr  7209  ctssdclemn0  7211  ctssdc  7214  enumctlemm  7215  enumct  7216  nnnninfeq2  7230  nninfisol  7234  enomnilem  7239  finomni  7241  ismkvnex  7256  enmkvlem  7262  enwomnilem  7270  nninfwlpoimlemg  7276  nninfwlpoimlemginf  7277  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  acnccim  7383  cauappcvgprlemm  7757  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdfu  7766  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  cauappcvgprlem2  7772  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemloc  7787  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgprlem2  7792  caucvgprprlemnkltj  7801  caucvgprprlemnkeqj  7802  caucvgprprlemnbj  7805  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemloc  7815  caucvgprprlemexbt  7818  caucvgprprlemexb  7819  caucvgprprlemaddq  7820  caucvgprprlem1  7821  caucvgprprlem2  7822  caucvgsrlemcau  7905  caucvgsrlemgt1  7907  caucvgsrlemoffcau  7910  caucvgsrlemoffres  7912  caucvgsr  7914  axcaucvglemval  8009  axcaucvglemcau  8010  axcaucvglemres  8011  fseq1p1m1  10215  4fvwrd4  10261  fvinim0ffz  10368  frecuzrdgg  10559  frecuzrdgsuctlem  10566  seq3val  10603  seqvalcd  10604  seq3p1  10608  seqp1cd  10613  ser3mono  10630  seq3split  10631  seq3caopr2  10636  iseqf1olemkle  10640  iseqf1olemklt  10641  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemmo  10648  iseqf1olemqk  10650  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  iseqf1olemfvp  10653  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemqsum  10656  seq3f1olemstep  10657  seq3f1oleml  10659  seq3f1o  10660  seqf1oglem2a  10661  seqf1oglem1  10662  seqf1oglem2  10663  seq3z  10671  seq3distr  10675  ser3ge0  10679  ser3le  10680  exp3vallem  10683  exp3val  10684  bcval5  10906  hashfz1  10926  resunimafz0  10974  leisorel  10980  zfz1isolemiso  10982  seq3coll  10985  ccatcl  11047  caucvgrelemcau  11262  caucvgre  11263  cvg1nlemf  11265  cvg1nlemcau  11266  cvg1nlemres  11267  recvguniqlem  11276  resqrexlemdecn  11294  resqrexlemcalc3  11298  resqrexlemnmsq  11299  resqrexlemnm  11300  resqrexlemcvg  11301  resqrexlemoverl  11303  resqrexlemglsq  11304  resqrexlemga  11305  clim2ser  11619  clim2ser2  11620  climrecvg1n  11630  climcvg1nlem  11631  serf0  11634  sumeq2  11641  fsum3cvg  11660  summodclem2a  11663  fsum3  11669  fisumss  11674  fsumcl2lem  11680  fsumadd  11688  fsummulc2  11730  fsumrelem  11753  isumshft  11772  cvgratnnlemseq  11808  cvgratnnlemrate  11812  clim2prod  11821  clim2divap  11822  prodfrecap  11828  prodfdivap  11829  ntrivcvgap  11830  prodeq2  11839  fproddccvg  11854  prodmodclem3  11857  prodmodclem2a  11858  fprodseq  11865  fprodssdc  11872  fprodmul  11873  effsumlt  11974  nninfctlemfo  12332  nn0seqcvgd  12334  ialgrlem1st  12335  eulerthlemrprm  12522  eulerthlema  12523  eulerthlemh  12524  pcmpt2  12638  pcmptdvds  12639  1arithlem4  12660  1arith  12661  ennnfonelemdc  12741  ennnfonelemjn  12744  ennnfonelemg  12745  ennnfonelemp1  12748  ennnfonelemom  12750  ennnfonelemhdmp1  12751  ennnfonelemss  12752  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemex  12756  ennnfonelemhom  12757  ennnfonelemnn0  12764  ennnfonelemim  12766  ctinfomlemom  12769  ctiunctlemudc  12779  ctiunctlemf  12780  ctiunctlemfo  12781  ssnnctlemct  12788  nninfdclemp1  12792  nninfdclemlt  12793  imasmnd2  13255  mhmf1o  13273  mhmco  13293  gsumfzcl  13302  isgrpinv  13357  pwssub  13416  imasgrp2  13417  mhmid  13422  mhmmnd  13423  ghmgrp  13425  mulgval  13429  mulgfng  13431  mulgnnsubcl  13441  ghmid  13556  ghminv  13557  ghmmulg  13563  ghmnsgpreima  13576  ghmeqker  13578  ghmf1  13580  kerf1ghm  13581  ghmf1o  13582  imasring  13797  rhmopp  13909  lspcl  14124  znidomb  14391  znrrg  14393  psrbaglesuppg  14405  psrbagfi  14406  mplsubgfilemcl  14432  iscnp4  14661  cnptopco  14665  lmtopcnp  14693  upxp  14715  uptx  14717  txlm  14722  comet  14942  metcnp3  14954  metcnp  14955  metcnp2  14956  metcnpi3  14960  elcncf2  15017  cncfco  15034  ivthreinc  15088  limcimolemlt  15107  cnplimcim  15110  cnplimclemle  15111  cnplimclemr  15112  limccnpcntop  15118  dvlemap  15123  dvcnp2cntop  15142  dvaddxxbr  15144  dvmulxxbr  15145  dvcoapbr  15150  dvcjbr  15151  dvef  15170  plyaddlem1  15190  plymullem1  15191  plycoeid3  15200  plycolemc  15201  plycjlemc  15203  plycj  15204  plycn  15205  plyrecj  15206  dvply1  15208  dvply2g  15209  lgsval  15452  lgscllem  15455  lgsval2lem  15458  lgsval4a  15470  lgsneg  15472  lgsdir  15483  lgsdilem2  15484  lgsdi  15485  lgsne0  15486  lgseisenlem3  15520  lgseisenlem4  15521  1dom1el  15889  2omap  15894  pwle2  15897  subctctexmid  15899  nnsf  15904  peano4nninf  15905  nninfalllem1  15907  nninfsellemdc  15909  nninfsellemeq  15913  nninfsellemqall  15914  nninfsellemeqinf  15915  nninfomnilem  15917  nnnninfex  15921  nninfnfiinf  15922  isomninnlem  15931  trilpolemeq1  15941  trilpolemlt1  15942  iswomninnlem  15950  iswomni0  15952  ismkvnnlem  15953  nconstwlpolemgt0  15965  nconstwlpolem  15966