Theorem ffvelcdmd 5716

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 5715	. 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 2176   -->wf 5267   ` cfv 5271

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279

This theorem is referenced by:  isotr  5885  caofinvl  6184  rdgon  6472  frecabcl  6485  phplem4dom  6959  fidceq  6966  dif1en  6976  fin0  6982  fin0or  6983  infm  7001  en2eqpr  7004  fidcenumlemrks  7055  fidcenumlemr  7057  supisoti  7112  ordiso2  7137  updjudhcoinlf  7182  updjudhcoinrg  7183  caseinl  7193  caseinr  7194  difinfsnlem  7201  difinfsn  7202  ctmlemr  7210  ctssdclemn0  7212  ctssdc  7215  enumctlemm  7216  enumct  7217  nnnninfeq2  7231  nninfisol  7235  enomnilem  7240  finomni  7242  ismkvnex  7257  enmkvlem  7263  enwomnilem  7271  nninfwlpoimlemg  7277  nninfwlpoimlemginf  7278  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  acnccim  7384  cauappcvgprlemm  7758  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdfu  7767  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlem2  7773  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemloc  7788  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgprlem2  7793  caucvgprprlemnkltj  7802  caucvgprprlemnkeqj  7803  caucvgprprlemnbj  7806  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemloc  7816  caucvgprprlemexbt  7819  caucvgprprlemexb  7820  caucvgprprlemaddq  7821  caucvgprprlem1  7822  caucvgprprlem2  7823  caucvgsrlemcau  7906  caucvgsrlemgt1  7908  caucvgsrlemoffcau  7911  caucvgsrlemoffres  7913  caucvgsr  7915  axcaucvglemval  8010  axcaucvglemcau  8011  axcaucvglemres  8012  fseq1p1m1  10216  4fvwrd4  10262  fvinim0ffz  10370  frecuzrdgg  10561  frecuzrdgsuctlem  10568  seq3val  10605  seqvalcd  10606  seq3p1  10610  seqp1cd  10615  ser3mono  10632  seq3split  10633  seq3caopr2  10638  iseqf1olemkle  10642  iseqf1olemklt  10643  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemmo  10650  iseqf1olemqk  10652  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  seq3f1olemstep  10659  seq3f1oleml  10661  seq3f1o  10662  seqf1oglem2a  10663  seqf1oglem1  10664  seqf1oglem2  10665  seq3z  10673  seq3distr  10677  ser3ge0  10681  ser3le  10682  exp3vallem  10685  exp3val  10686  bcval5  10908  hashfz1  10928  resunimafz0  10976  leisorel  10982  zfz1isolemiso  10984  seq3coll  10987  ccatcl  11049  swrdclg  11103  caucvgrelemcau  11291  caucvgre  11292  cvg1nlemf  11294  cvg1nlemcau  11295  cvg1nlemres  11296  recvguniqlem  11305  resqrexlemdecn  11323  resqrexlemcalc3  11327  resqrexlemnmsq  11328  resqrexlemnm  11329  resqrexlemcvg  11330  resqrexlemoverl  11332  resqrexlemglsq  11333  resqrexlemga  11334  clim2ser  11648  clim2ser2  11649  climrecvg1n  11659  climcvg1nlem  11660  serf0  11663  sumeq2  11670  fsum3cvg  11689  summodclem2a  11692  fsum3  11698  fisumss  11703  fsumcl2lem  11709  fsumadd  11717  fsummulc2  11759  fsumrelem  11782  isumshft  11801  cvgratnnlemseq  11837  cvgratnnlemrate  11841  clim2prod  11850  clim2divap  11851  prodfrecap  11857  prodfdivap  11858  ntrivcvgap  11859  prodeq2  11868  fproddccvg  11883  prodmodclem3  11886  prodmodclem2a  11887  fprodseq  11894  fprodssdc  11901  fprodmul  11902  effsumlt  12003  nninfctlemfo  12361  nn0seqcvgd  12363  ialgrlem1st  12364  eulerthlemrprm  12551  eulerthlema  12552  eulerthlemh  12553  pcmpt2  12667  pcmptdvds  12668  1arithlem4  12689  1arith  12690  ennnfonelemdc  12770  ennnfonelemjn  12773  ennnfonelemg  12774  ennnfonelemp1  12777  ennnfonelemom  12779  ennnfonelemhdmp1  12780  ennnfonelemss  12781  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemnn0  12793  ennnfonelemim  12795  ctinfomlemom  12798  ctiunctlemudc  12808  ctiunctlemf  12809  ctiunctlemfo  12810  ssnnctlemct  12817  nninfdclemp1  12821  nninfdclemlt  12822  imasmnd2  13284  mhmf1o  13302  mhmco  13322  gsumfzcl  13331  isgrpinv  13386  pwssub  13445  imasgrp2  13446  mhmid  13451  mhmmnd  13452  ghmgrp  13454  mulgval  13458  mulgfng  13460  mulgnnsubcl  13470  ghmid  13585  ghminv  13586  ghmmulg  13592  ghmnsgpreima  13605  ghmeqker  13607  ghmf1  13609  kerf1ghm  13610  ghmf1o  13611  imasring  13826  rhmopp  13938  lspcl  14153  znidomb  14420  znrrg  14422  psrbaglesuppg  14434  psrbagfi  14435  mplsubgfilemcl  14461  iscnp4  14690  cnptopco  14694  lmtopcnp  14722  upxp  14744  uptx  14746  txlm  14751  comet  14971  metcnp3  14983  metcnp  14984  metcnp2  14985  metcnpi3  14989  elcncf2  15046  cncfco  15063  ivthreinc  15117  limcimolemlt  15136  cnplimcim  15139  cnplimclemle  15140  cnplimclemr  15141  limccnpcntop  15147  dvlemap  15152  dvcnp2cntop  15171  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvcjbr  15180  dvef  15199  plyaddlem1  15219  plymullem1  15220  plycoeid3  15229  plycolemc  15230  plycjlemc  15232  plycj  15233  plycn  15234  plyrecj  15235  dvply1  15237  dvply2g  15238  lgsval  15481  lgscllem  15484  lgsval2lem  15487  lgsval4a  15499  lgsneg  15501  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgseisenlem3  15549  lgseisenlem4  15550  1dom1el  15927  2omap  15932  pwle2  15935  subctctexmid  15937  nnsf  15942  peano4nninf  15943  nninfalllem1  15945  nninfsellemdc  15947  nninfsellemeq  15951  nninfsellemqall  15952  nninfsellemeqinf  15953  nninfomnilem  15955  nnnninfex  15959  nninfnfiinf  15960  isomninnlem  15969  trilpolemeq1  15979  trilpolemlt1  15980  iswomninnlem  15988  iswomni0  15990  ismkvnnlem  15991  nconstwlpolemgt0  16003  nconstwlpolem  16004