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  6662  frecabcl  6675  1dom1el  7113  phplem4dom  7169  fidceq  7177  dif1en  7189  fin0  7195  fin0or  7196  infm  7217  en2eqpr  7220  fidcenumlemrks  7277  fidcenumlemr  7279  funisfsuppdc  7298  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  10517  4fvwrd4  10563  fvinim0ffz  10676  frecuzrdgg  10873  frecuzrdgsuctlem  10880  seq3val  10917  seqvalcd  10918  seq3p1  10922  seqp1cd  10927  ser3mono  10944  seq3split  10945  seq3caopr2  10950  iseqf1olemkle  10954  iseqf1olemklt  10955  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemmo  10962  iseqf1olemqk  10964  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seq3f1olemstep  10971  seq3f1oleml  10973  seq3f1o  10974  seqf1oglem2a  10975  seqf1oglem1  10976  seqf1oglem2  10977  seq3z  10985  seq3distr  10989  ser3ge0  10993  ser3le  10994  exp3vallem  10997  exp3val  10998  bcval5  11222  hashfz1  11243  resunimafz0  11295  leisorel  11310  zfz1isolemiso  11312  seq3coll  11315  ccatcl  11382  swrdclg  11443  caucvgrelemcau  11767  caucvgre  11768  cvg1nlemf  11770  cvg1nlemcau  11771  cvg1nlemres  11772  recvguniqlem  11781  resqrexlemdecn  11799  resqrexlemcalc3  11803  resqrexlemnmsq  11804  resqrexlemnm  11805  resqrexlemcvg  11806  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemga  11810  fiidxsupcl  12017  clim2ser  12127  clim2ser2  12128  climrecvg1n  12138  climcvg1nlem  12139  serf0  12142  sumeq2  12149  fsum3cvg  12169  summodclem2a  12172  fsum3  12178  fisumss  12183  fsumcl2lem  12189  fsumadd  12197  fsummulc2  12239  fsumrelem  12262  isumshft  12281  cvgratnnlemseq  12317  cvgratnnlemrate  12321  clim2prod  12330  clim2divap  12331  prodfrecap  12337  prodfdivap  12338  ntrivcvgap  12339  prodeq2  12348  fproddccvg  12363  prodmodclem3  12366  prodmodclem2a  12367  fprodseq  12374  fprodssdc  12381  fprodmul  12382  effsumlt  12483  nninfctlemfo  12841  nn0seqcvgd  12843  ialgrlem1st  12844  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemh  13037  pcmpt2  13151  pcmptdvds  13152  1arithlem4  13173  1arith  13174  ennnfonelemdc  13347  ennnfonelemjn  13350  ennnfonelemg  13351  ennnfonelemp1  13354  ennnfonelemom  13356  ennnfonelemhdmp1  13357  ennnfonelemss  13358  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemnn0  13370  ennnfonelemim  13372  ctinfomlemom  13375  ctiunctlemudc  13385  ctiunctlemf  13386  ctiunctlemfo  13387  ssnnctlemct  13394  nninfdclemp1  13398  nninfdclemlt  13399  imasmnd2  13817  mhmf1o  13835  mhmco  13855  gzsumcl  13862  isgrpinv  13917  imasgrp2  13971  mhmid  13976  mhmmnd  13977  ghmgrp  13979  mulgval  13983  mulgfng  13985  mulgnnsubcl  13995  ghmid  14110  ghminv  14111  ghmmulg  14117  ghmnsgpreima  14130  ghmeqker  14132  ghmf1  14134  kerf1ghm  14135  ghmf1o  14136  gzsumsplit0  14237  gsumvalfi  14241  gsumclfi  14248  gsumsubmclfi  14252  gsumresfi  14262  pwssub  14322  imasring  14477  rhmopp  14591  lspcl  14836  znidomb  15101  znrrg  15103  asclelbas  15134  psrbagfi  15166  psrbaglesuppg  15170  psrbaglecl  15172  psrbagcon  15174  psrbaglefifi  15175  psrbagmaxlem1  15178  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  rhmpsrfilem2  15194  psrmulvalfi  15197  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  psrdifi  15211  psrdirfi  15212  mvrcl2fi  15220  iscnp4  15461  cnptopco  15465  lmtopcnp  15493  upxp  15515  uptx  15517  txlm  15522  comet  15742  metcnp3  15754  metcnp  15755  metcnp2  15756  metcnpi3  15760  elcncf2  15817  cncfco  15834  ivthreinc  15888  limcimolemlt  15907  cnplimcim  15910  cnplimclemle  15911  cnplimclemr  15912  limccnpcntop  15918  dvlemap  15923  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvef  15970  plyaddlem1  15990  plymullem1  15991  plycoeid3  16000  plycolemc  16001  plycjlemc  16003  plycj  16004  plycn  16005  plyrecj  16006  dvply1  16008  dvply2g  16009  logfac  16143  bposlem3  16330  bposlem5  16332  bposlem6  16333  bposlem9  16336  lgsval  16345  lgscllem  16348  lgsval2lem  16351  lgsval4a  16363  lgsneg  16365  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  lgseisenlem3  16413  lgseisenlem4  16414  p1evtxdeqfi  16775  wlkvtxm  16803  wlkvtxiedg  16808  wlkvtxiedgg  16809  upgriswlkdc  16823  trlsegvdeglem7  16929  trlsegvdegfi  16930  eupth2lem3lem1fi  16931  eupth2lem3lem2fi  16932  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936  eupth2lem3lem7fi  16937  eupth2lemsfi  16941  3dom  17240  pwle2  17250  subctctexmid  17252  nnsf  17271  peano4nninf  17272  nninfalllem1  17274  nninfsellemdc  17276  nninfsellemeq  17280  nninfsellemqall  17281  nninfsellemeqinf  17282  nninfomnilem  17284  nnnninfex  17288  nninfnfiinf  17289  repiecelem  17297  repiecele0  17298  repiecege0  17299  isomninnlem  17302  trilpolemeq1  17313  trilpolemlt1  17314  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326  nconstwlpolemgt0  17338  nconstwlpolem  17339