Theorem ffvelcdmd 5694

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 5693	. 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 2164   -->wf 5250   ` cfv 5254

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-sbc 2986  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-fv 5262

This theorem is referenced by:  isotr  5859  caofinvl  6155  rdgon  6439  frecabcl  6452  phplem4dom  6918  fidceq  6925  dif1en  6935  fin0  6941  fin0or  6942  infm  6960  en2eqpr  6963  fidcenumlemrks  7012  fidcenumlemr  7014  supisoti  7069  ordiso2  7094  updjudhcoinlf  7139  updjudhcoinrg  7140  caseinl  7150  caseinr  7151  difinfsnlem  7158  difinfsn  7159  ctmlemr  7167  ctssdclemn0  7169  ctssdc  7172  enumctlemm  7173  enumct  7174  nnnninfeq2  7188  nninfisol  7192  enomnilem  7197  finomni  7199  ismkvnex  7214  enmkvlem  7220  enwomnilem  7228  nninfwlpoimlemg  7234  nninfwlpoimlemginf  7235  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  cauappcvgprlemm  7705  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfu  7714  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlem2  7720  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgprlem2  7740  caucvgprprlemnkltj  7749  caucvgprprlemnkeqj  7750  caucvgprprlemnbj  7753  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemloc  7763  caucvgprprlemexbt  7766  caucvgprprlemexb  7767  caucvgprprlemaddq  7768  caucvgprprlem1  7769  caucvgprprlem2  7770  caucvgsrlemcau  7853  caucvgsrlemgt1  7855  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  caucvgsr  7862  axcaucvglemval  7957  axcaucvglemcau  7958  axcaucvglemres  7959  fseq1p1m1  10160  4fvwrd4  10206  fvinim0ffz  10308  frecuzrdgg  10487  frecuzrdgsuctlem  10494  seq3val  10531  seqvalcd  10532  seq3p1  10536  seqp1cd  10541  ser3mono  10558  seq3split  10559  seq3caopr2  10564  iseqf1olemkle  10568  iseqf1olemklt  10569  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemmo  10576  iseqf1olemqk  10578  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seq3f1olemstep  10585  seq3f1oleml  10587  seq3f1o  10588  seqf1oglem2a  10589  seqf1oglem1  10590  seqf1oglem2  10591  seq3z  10599  seq3distr  10603  ser3ge0  10607  ser3le  10608  exp3vallem  10611  exp3val  10612  bcval5  10834  hashfz1  10854  resunimafz0  10902  leisorel  10908  zfz1isolemiso  10910  seq3coll  10913  caucvgrelemcau  11124  caucvgre  11125  cvg1nlemf  11127  cvg1nlemcau  11128  cvg1nlemres  11129  recvguniqlem  11138  resqrexlemdecn  11156  resqrexlemcalc3  11160  resqrexlemnmsq  11161  resqrexlemnm  11162  resqrexlemcvg  11163  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemga  11167  clim2ser  11480  clim2ser2  11481  climrecvg1n  11491  climcvg1nlem  11492  serf0  11495  sumeq2  11502  fsum3cvg  11521  summodclem2a  11524  fsum3  11530  fisumss  11535  fsumcl2lem  11541  fsumadd  11549  fsummulc2  11591  fsumrelem  11614  isumshft  11633  cvgratnnlemseq  11669  cvgratnnlemrate  11673  clim2prod  11682  clim2divap  11683  prodfrecap  11689  prodfdivap  11690  ntrivcvgap  11691  prodeq2  11700  fproddccvg  11715  prodmodclem3  11718  prodmodclem2a  11719  fprodseq  11726  fprodssdc  11733  fprodmul  11734  effsumlt  11835  nninfctlemfo  12177  nn0seqcvgd  12179  ialgrlem1st  12180  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemh  12369  pcmpt2  12482  pcmptdvds  12483  1arithlem4  12504  1arith  12505  ennnfonelemdc  12556  ennnfonelemjn  12559  ennnfonelemg  12560  ennnfonelemp1  12563  ennnfonelemom  12565  ennnfonelemhdmp1  12566  ennnfonelemss  12567  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemnn0  12579  ennnfonelemim  12581  ctinfomlemom  12584  ctiunctlemudc  12594  ctiunctlemf  12595  ctiunctlemfo  12596  ssnnctlemct  12603  nninfdclemp1  12607  nninfdclemlt  12608  mhmf1o  13042  mhmco  13062  gsumfzcl  13071  isgrpinv  13126  imasgrp2  13180  mhmid  13185  mhmmnd  13186  ghmgrp  13188  mulgval  13192  mulgfng  13194  mulgnnsubcl  13204  ghmid  13319  ghminv  13320  ghmmulg  13326  ghmnsgpreima  13339  ghmeqker  13341  ghmf1  13343  kerf1ghm  13344  ghmf1o  13345  imasring  13560  rhmopp  13672  lspcl  13887  znidomb  14146  znrrg  14148  psrbaglesuppg  14158  iscnp4  14386  cnptopco  14390  lmtopcnp  14418  upxp  14440  uptx  14442  txlm  14447  comet  14667  metcnp3  14679  metcnp  14680  metcnp2  14681  metcnpi3  14685  elcncf2  14729  cncfco  14746  ivthreinc  14799  limcimolemlt  14818  cnplimcim  14821  cnplimclemle  14822  cnplimclemr  14823  limccnpcntop  14829  dvlemap  14834  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvef  14873  plyaddlem1  14893  plymullem1  14894  lgsval  15120  lgscllem  15123  lgsval2lem  15126  lgsval4a  15138  lgsneg  15140  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  lgseisenlem3  15188  lgseisenlem4  15189  1dom1el  15483  pwle2  15489  subctctexmid  15491  nnsf  15495  peano4nninf  15496  nninfalllem1  15498  nninfsellemdc  15500  nninfsellemeq  15504  nninfsellemqall  15505  nninfsellemeqinf  15506  nninfomnilem  15508  isomninnlem  15520  trilpolemeq1  15530  trilpolemlt1  15531  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542  nconstwlpolemgt0  15554  nconstwlpolem  15555