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  mplsubgfilemcl  15212  iscnp4  15441  cnptopco  15445  lmtopcnp  15473  upxp  15495  uptx  15497  txlm  15502  comet  15722  metcnp3  15734  metcnp  15735  metcnp2  15736  metcnpi3  15740  elcncf2  15797  cncfco  15814  ivthreinc  15868  limcimolemlt  15887  cnplimcim  15890  cnplimclemle  15891  cnplimclemr  15892  limccnpcntop  15898  dvlemap  15903  dvcnp2cntop  15922  dvaddxxbr  15924  dvmulxxbr  15925  dvcoapbr  15930  dvcjbr  15931  dvef  15950  plyaddlem1  15970  plymullem1  15971  plycoeid3  15980  plycolemc  15981  plycjlemc  15983  plycj  15984  plycn  15985  plyrecj  15986  dvply1  15988  dvply2g  15989  logfac  16123  bposlem3  16310  bposlem5  16312  bposlem6  16313  bposlem9  16316  lgsval  16325  lgscllem  16328  lgsval2lem  16331  lgsval4a  16343  lgsneg  16345  lgsdir  16356  lgsdilem2  16357  lgsdi  16358  lgsne0  16359  lgseisenlem3  16393  lgseisenlem4  16394  p1evtxdeqfi  16755  wlkvtxm  16783  wlkvtxiedg  16788  wlkvtxiedgg  16789  upgriswlkdc  16803  trlsegvdeglem7  16909  trlsegvdegfi  16910  eupth2lem3lem1fi  16911  eupth2lem3lem2fi  16912  eupth2lem3lem3fi  16913  eupth2lem3lem6fi  16914  eupth2lem3lem4fi  16916  eupth2lem3lem7fi  16917  eupth2lemsfi  16921  3dom  17220  pwle2  17230  subctctexmid  17232  nnsf  17251  peano4nninf  17252  nninfalllem1  17254  nninfsellemdc  17256  nninfsellemeq  17260  nninfsellemqall  17261  nninfsellemeqinf  17262  nninfomnilem  17264  nnnninfex  17268  nninfnfiinf  17269  repiecelem  17277  repiecele0  17278  repiecege0  17279  isomninnlem  17282  trilpolemeq1  17293  trilpolemlt1  17294  iswomninnlem  17303  iswomni0  17305  ismkvnnlem  17306  nconstwlpolemgt0  17318  nconstwlpolem  17319