Theorem ffvelcdmd 5847

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 5846	. 2 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )
4	1, 3	mpdan 425	1 |- ( ph -> ( F ` C ) e. B )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   -->wf 5376   ` cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-fv 5388

This theorem is used by:  isotr  6025  caofinvl  6332  fvdifsuppst  6488  rdgon  6661  frecabcl  6674  1dom1el  7111  phplem4dom  7167  fidceq  7175  dif1en  7187  fin0  7193  fin0or  7194  infm  7215  en2eqpr  7218  fidcenumlemrks  7275  fidcenumlemr  7277  fdcf1  7321  2omap  7324  supisoti  7356  ordiso2  7381  updjudhcoinlf  7426  updjudhcoinrg  7427  caseinl  7437  caseinr  7438  difinfsnlem  7445  difinfsn  7446  ctmlemr  7454  ctssdclemn0  7456  ctssdc  7459  enumctlemm  7460  enumct  7461  nnnninfeq2  7475  nninfisol  7479  enomnilem  7484  finomni  7486  ismkvnex  7501  enmkvlem  7507  enwomnilem  7515  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  pr2cv1  7547  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acnccim  7644  cauappcvgprlemm  8018  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlem2  8033  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem1  8052  caucvgprlem2  8053  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemnbj  8066  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  caucvgprprlemexb  8080  caucvgprprlemaddq  8081  caucvgprprlem1  8082  caucvgprprlem2  8083  caucvgsrlemcau  8166  caucvgsrlemgt1  8168  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  caucvgsr  8175  axcaucvglemval  8270  axcaucvglemcau  8271  axcaucvglemres  8272  fseq1p1m1  10518  4fvwrd4  10564  fvinim0ffz  10677  frecuzrdgg  10874  frecuzrdgsuctlem  10881  seq3val  10918  seqvalcd  10919  seq3p1  10923  seqp1cd  10928  ser3mono  10945  seq3split  10946  seq3caopr2  10951  iseqf1olemkle  10955  iseqf1olemklt  10956  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemmo  10963  iseqf1olemqk  10965  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seq3f1olemstep  10972  seq3f1oleml  10974  seq3f1o  10975  seqf1oglem2a  10976  seqf1oglem1  10977  seqf1oglem2  10978  seq3z  10986  seq3distr  10990  ser3ge0  10994  ser3le  10995  exp3vallem  10998  exp3val  10999  bcval5  11223  hashfz1  11244  resunimafz0  11296  leisorel  11311  zfz1isolemiso  11313  seq3coll  11316  ccatcl  11383  swrdclg  11444  caucvgrelemcau  11768  caucvgre  11769  cvg1nlemf  11771  cvg1nlemcau  11772  cvg1nlemres  11773  recvguniqlem  11782  resqrexlemdecn  11800  resqrexlemcalc3  11804  resqrexlemnmsq  11805  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemga  11811  fiidxsupcl  12018  clim2ser  12128  clim2ser2  12129  climrecvg1n  12139  climcvg1nlem  12140  serf0  12143  sumeq2  12150  fsum3cvg  12170  summodclem2a  12173  fsum3  12179  fisumss  12184  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  fsumrelem  12263  isumshft  12282  cvgratnnlemseq  12318  cvgratnnlemrate  12322  clim2prod  12331  clim2divap  12332  prodfrecap  12338  prodfdivap  12339  ntrivcvgap  12340  prodeq2  12349  fproddccvg  12364  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  fprodssdc  12382  fprodmul  12383  effsumlt  12484  nninfctlemfo  12842  nn0seqcvgd  12844  ialgrlem1st  12845  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  pcmpt2  13152  pcmptdvds  13153  1arithlem4  13174  1arith  13175  ennnfonelemdc  13348  ennnfonelemjn  13351  ennnfonelemg  13352  ennnfonelemp1  13355  ennnfonelemom  13357  ennnfonelemhdmp1  13358  ennnfonelemss  13359  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemnn0  13371  ennnfonelemim  13373  ctinfomlemom  13376  ctiunctlemudc  13386  ctiunctlemf  13387  ctiunctlemfo  13388  ssnnctlemct  13395  nninfdclemp1  13399  nninfdclemlt  13400  imasmnd2  13818  mhmf1o  13836  mhmco  13856  gzsumcl  13863  isgrpinv  13918  imasgrp2  13972  mhmid  13977  mhmmnd  13978  ghmgrp  13980  mulgval  13984  mulgfng  13986  mulgnnsubcl  13996  ghmid  14111  ghminv  14112  ghmmulg  14118  ghmnsgpreima  14131  ghmeqker  14133  ghmf1  14135  kerf1ghm  14136  ghmf1o  14137  gzsumsplit0  14238  gsumvalfi  14242  gsumclfi  14249  gsumsubmclfi  14253  gsumresfi  14263  pwssub  14323  imasring  14478  rhmopp  14592  lspcl  14837  znidomb  15102  znrrg  15104  asclelbas  15135  psrbaglesuppg  15166  psrbagfi  15168  psrbaglecl  15169  psrbagcon  15171  psrbaglefifi  15172  rhmpsrfilem2  15185  psrmulvalfi  15188  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  psrdifi  15202  psrdirfi  15203  mplsubgfilemcl  15215  iscnp4  15444  cnptopco  15448  lmtopcnp  15476  upxp  15498  uptx  15500  txlm  15505  comet  15725  metcnp3  15737  metcnp  15738  metcnp2  15739  metcnpi3  15743  elcncf2  15800  cncfco  15817  ivthreinc  15871  limcimolemlt  15890  cnplimcim  15893  cnplimclemle  15894  cnplimclemr  15895  limccnpcntop  15901  dvlemap  15906  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvef  15953  plyaddlem1  15973  plymullem1  15974  plycoeid3  15983  plycolemc  15984  plycjlemc  15986  plycj  15987  plycn  15988  plyrecj  15989  dvply1  15991  dvply2g  15992  logfac  16126  bposlem3  16313  bposlem5  16315  bposlem6  16316  bposlem9  16319  lgsval  16328  lgscllem  16331  lgsval2lem  16334  lgsval4a  16346  lgsneg  16348  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  lgseisenlem3  16396  lgseisenlem4  16397  p1evtxdeqfi  16758  wlkvtxm  16786  wlkvtxiedg  16791  wlkvtxiedgg  16792  upgriswlkdc  16806  trlsegvdeglem7  16912  trlsegvdegfi  16913  eupth2lem3lem1fi  16914  eupth2lem3lem2fi  16915  eupth2lem3lem3fi  16916  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  eupth2lem3lem7fi  16920  eupth2lemsfi  16924  3dom  17223  pwle2  17233  subctctexmid  17235  nnsf  17254  peano4nninf  17255  nninfalllem1  17257  nninfsellemdc  17259  nninfsellemeq  17263  nninfsellemqall  17264  nninfsellemeqinf  17265  nninfomnilem  17267  nnnninfex  17271  nninfnfiinf  17272  repiecelem  17280  repiecele0  17281  repiecege0  17282  isomninnlem  17285  trilpolemeq1  17296  trilpolemlt1  17297  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309  nconstwlpolemgt0  17321  nconstwlpolem  17322