Theorem ffvelcdmd 5783

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 5782	. 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 2202   -->wf 5322   ` cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334

This theorem is referenced by:  isotr  5956  caofinvl  6260  rdgon  6551  frecabcl  6564  1dom1el  6992  phplem4dom  7047  fidceq  7055  dif1en  7067  fin0  7073  fin0or  7074  infm  7095  en2eqpr  7098  fidcenumlemrks  7151  fidcenumlemr  7153  supisoti  7208  ordiso2  7233  updjudhcoinlf  7278  updjudhcoinrg  7279  caseinl  7289  caseinr  7290  difinfsnlem  7297  difinfsn  7298  ctmlemr  7306  ctssdclemn0  7308  ctssdc  7311  enumctlemm  7312  enumct  7313  nnnninfeq2  7327  nninfisol  7331  enomnilem  7336  finomni  7338  ismkvnex  7353  enmkvlem  7359  enwomnilem  7367  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  pr2cv1  7399  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  acnccim  7490  cauappcvgprlemm  7864  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfu  7873  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlem2  7879  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgprlem2  7899  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  caucvgprprlemnbj  7912  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemloc  7922  caucvgprprlemexbt  7925  caucvgprprlemexb  7926  caucvgprprlemaddq  7927  caucvgprprlem1  7928  caucvgprprlem2  7929  caucvgsrlemcau  8012  caucvgsrlemgt1  8014  caucvgsrlemoffcau  8017  caucvgsrlemoffres  8019  caucvgsr  8021  axcaucvglemval  8116  axcaucvglemcau  8117  axcaucvglemres  8118  fseq1p1m1  10328  4fvwrd4  10374  fvinim0ffz  10486  frecuzrdgg  10677  frecuzrdgsuctlem  10684  seq3val  10721  seqvalcd  10722  seq3p1  10726  seqp1cd  10731  ser3mono  10748  seq3split  10749  seq3caopr2  10754  iseqf1olemkle  10758  iseqf1olemklt  10759  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemmo  10766  iseqf1olemqk  10768  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seq3f1olemstep  10775  seq3f1oleml  10777  seq3f1o  10778  seqf1oglem2a  10779  seqf1oglem1  10780  seqf1oglem2  10781  seq3z  10789  seq3distr  10793  ser3ge0  10797  ser3le  10798  exp3vallem  10801  exp3val  10802  bcval5  11024  hashfz1  11044  resunimafz0  11094  leisorel  11100  zfz1isolemiso  11102  seq3coll  11105  ccatcl  11169  swrdclg  11230  caucvgrelemcau  11540  caucvgre  11541  cvg1nlemf  11543  cvg1nlemcau  11544  cvg1nlemres  11545  recvguniqlem  11554  resqrexlemdecn  11572  resqrexlemcalc3  11576  resqrexlemnmsq  11577  resqrexlemnm  11578  resqrexlemcvg  11579  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemga  11583  clim2ser  11897  clim2ser2  11898  climrecvg1n  11908  climcvg1nlem  11909  serf0  11912  sumeq2  11919  fsum3cvg  11938  summodclem2a  11941  fsum3  11947  fisumss  11952  fsumcl2lem  11958  fsumadd  11966  fsummulc2  12008  fsumrelem  12031  isumshft  12050  cvgratnnlemseq  12086  cvgratnnlemrate  12090  clim2prod  12099  clim2divap  12100  prodfrecap  12106  prodfdivap  12107  ntrivcvgap  12108  prodeq2  12117  fproddccvg  12132  prodmodclem3  12135  prodmodclem2a  12136  fprodseq  12143  fprodssdc  12150  fprodmul  12151  effsumlt  12252  nninfctlemfo  12610  nn0seqcvgd  12612  ialgrlem1st  12613  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  pcmpt2  12916  pcmptdvds  12917  1arithlem4  12938  1arith  12939  ennnfonelemdc  13019  ennnfonelemjn  13022  ennnfonelemg  13023  ennnfonelemp1  13026  ennnfonelemom  13028  ennnfonelemhdmp1  13029  ennnfonelemss  13030  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemnn0  13042  ennnfonelemim  13044  ctinfomlemom  13047  ctiunctlemudc  13057  ctiunctlemf  13058  ctiunctlemfo  13059  ssnnctlemct  13066  nninfdclemp1  13070  nninfdclemlt  13071  imasmnd2  13534  mhmf1o  13552  mhmco  13572  gsumfzcl  13581  isgrpinv  13636  pwssub  13695  imasgrp2  13696  mhmid  13701  mhmmnd  13702  ghmgrp  13704  mulgval  13708  mulgfng  13710  mulgnnsubcl  13720  ghmid  13835  ghminv  13836  ghmmulg  13842  ghmnsgpreima  13855  ghmeqker  13857  ghmf1  13859  kerf1ghm  13860  ghmf1o  13861  imasring  14076  rhmopp  14189  lspcl  14404  znidomb  14671  znrrg  14673  psrbaglesuppg  14685  psrbagfi  14686  mplsubgfilemcl  14712  iscnp4  14941  cnptopco  14945  lmtopcnp  14973  upxp  14995  uptx  14997  txlm  15002  comet  15222  metcnp3  15234  metcnp  15235  metcnp2  15236  metcnpi3  15240  elcncf2  15297  cncfco  15314  ivthreinc  15368  limcimolemlt  15387  cnplimcim  15390  cnplimclemle  15391  cnplimclemr  15392  limccnpcntop  15398  dvlemap  15403  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvef  15450  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  plycolemc  15481  plycjlemc  15483  plycj  15484  plycn  15485  plyrecj  15486  dvply1  15488  dvply2g  15489  lgsval  15732  lgscllem  15735  lgsval2lem  15738  lgsval4a  15750  lgsneg  15752  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgseisenlem3  15800  lgseisenlem4  15801  p1evtxdeqfi  16162  wlkvtxm  16190  wlkvtxiedg  16195  wlkvtxiedgg  16196  upgriswlkdc  16210  trlsegvdeglem7  16316  3dom  16587  2omap  16594  pwle2  16599  subctctexmid  16601  nnsf  16607  peano4nninf  16608  nninfalllem1  16610  nninfsellemdc  16612  nninfsellemeq  16616  nninfsellemqall  16617  nninfsellemeqinf  16618  nninfomnilem  16620  nnnninfex  16624  nninfnfiinf  16625  isomninnlem  16634  trilpolemeq1  16644  trilpolemlt1  16645  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656  nconstwlpolemgt0  16668  nconstwlpolem  16669  gfsumval  16680