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  11233  caucvgre  11234  cvg1nlemf  11236  cvg1nlemcau  11237  cvg1nlemres  11238  recvguniqlem  11247  resqrexlemdecn  11265  resqrexlemcalc3  11269  resqrexlemnmsq  11270  resqrexlemnm  11271  resqrexlemcvg  11272  resqrexlemoverl  11274  resqrexlemglsq  11275  resqrexlemga  11276  clim2ser  11590  clim2ser2  11591  climrecvg1n  11601  climcvg1nlem  11602  serf0  11605  sumeq2  11612  fsum3cvg  11631  summodclem2a  11634  fsum3  11640  fisumss  11645  fsumcl2lem  11651  fsumadd  11659  fsummulc2  11701  fsumrelem  11724  isumshft  11743  cvgratnnlemseq  11779  cvgratnnlemrate  11783  clim2prod  11792  clim2divap  11793  prodfrecap  11799  prodfdivap  11800  ntrivcvgap  11801  prodeq2  11810  fproddccvg  11825  prodmodclem3  11828  prodmodclem2a  11829  fprodseq  11836  fprodssdc  11843  fprodmul  11844  effsumlt  11945  nninfctlemfo  12303  nn0seqcvgd  12305  ialgrlem1st  12306  eulerthlemrprm  12493  eulerthlema  12494  eulerthlemh  12495  pcmpt2  12609  pcmptdvds  12610  1arithlem4  12631  1arith  12632  ennnfonelemdc  12712  ennnfonelemjn  12715  ennnfonelemg  12716  ennnfonelemp1  12719  ennnfonelemom  12721  ennnfonelemhdmp1  12722  ennnfonelemss  12723  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemex  12727  ennnfonelemhom  12728  ennnfonelemnn0  12735  ennnfonelemim  12737  ctinfomlemom  12740  ctiunctlemudc  12750  ctiunctlemf  12751  ctiunctlemfo  12752  ssnnctlemct  12759  nninfdclemp1  12763  nninfdclemlt  12764  imasmnd2  13226  mhmf1o  13244  mhmco  13264  gsumfzcl  13273  isgrpinv  13328  pwssub  13387  imasgrp2  13388  mhmid  13393  mhmmnd  13394  ghmgrp  13396  mulgval  13400  mulgfng  13402  mulgnnsubcl  13412  ghmid  13527  ghminv  13528  ghmmulg  13534  ghmnsgpreima  13547  ghmeqker  13549  ghmf1  13551  kerf1ghm  13552  ghmf1o  13553  imasring  13768  rhmopp  13880  lspcl  14095  znidomb  14362  znrrg  14364  psrbaglesuppg  14376  psrbagfi  14377  mplsubgfilemcl  14403  iscnp4  14632  cnptopco  14636  lmtopcnp  14664  upxp  14686  uptx  14688  txlm  14693  comet  14913  metcnp3  14925  metcnp  14926  metcnp2  14927  metcnpi3  14931  elcncf2  14988  cncfco  15005  ivthreinc  15059  limcimolemlt  15078  cnplimcim  15081  cnplimclemle  15082  cnplimclemr  15083  limccnpcntop  15089  dvlemap  15094  dvcnp2cntop  15113  dvaddxxbr  15115  dvmulxxbr  15116  dvcoapbr  15121  dvcjbr  15122  dvef  15141  plyaddlem1  15161  plymullem1  15162  plycoeid3  15171  plycolemc  15172  plycjlemc  15174  plycj  15175  plycn  15176  plyrecj  15177  dvply1  15179  dvply2g  15180  lgsval  15423  lgscllem  15426  lgsval2lem  15429  lgsval4a  15441  lgsneg  15443  lgsdir  15454  lgsdilem2  15455  lgsdi  15456  lgsne0  15457  lgseisenlem3  15491  lgseisenlem4  15492  1dom1el  15860  2omap  15865  pwle2  15868  subctctexmid  15870  nnsf  15875  peano4nninf  15876  nninfalllem1  15878  nninfsellemdc  15880  nninfsellemeq  15884  nninfsellemqall  15885  nninfsellemeqinf  15886  nninfomnilem  15888  nnnninfex  15892  nninfnfiinf  15893  isomninnlem  15902  trilpolemeq1  15912  trilpolemlt1  15913  iswomninnlem  15921  iswomni0  15923  ismkvnnlem  15924  nconstwlpolemgt0  15936  nconstwlpolem  15937