Theorem ffvelcdmd 5844

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 5843	. 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 5373   ` cfv 5377

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 4249  ax-pow 4311  ax-pr 4346

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 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-fv 5385

This theorem is used by:  isotr  6022  caofinvl  6328  fvdifsuppst  6484  rdgon  6657  frecabcl  6670  1dom1el  7107  phplem4dom  7163  fidceq  7171  dif1en  7183  fin0  7189  fin0or  7190  infm  7211  en2eqpr  7214  fidcenumlemrks  7270  fidcenumlemr  7272  fdcf1  7316  2omap  7318  supisoti  7350  ordiso2  7375  updjudhcoinlf  7420  updjudhcoinrg  7421  caseinl  7431  caseinr  7432  difinfsnlem  7439  difinfsn  7440  ctmlemr  7448  ctssdclemn0  7450  ctssdc  7453  enumctlemm  7454  enumct  7455  nnnninfeq2  7469  nninfisol  7473  enomnilem  7478  finomni  7480  ismkvnex  7495  enmkvlem  7501  enwomnilem  7509  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  pr2cv1  7541  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acnccim  7638  cauappcvgprlemm  8012  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprlem2  8047  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnbj  8060  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemexb  8074  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  caucvgsr  8169  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  fseq1p1m1  10501  4fvwrd4  10547  fvinim0ffz  10660  frecuzrdgg  10853  frecuzrdgsuctlem  10860  seq3val  10897  seqvalcd  10898  seq3p1  10902  seqp1cd  10907  ser3mono  10924  seq3split  10925  seq3caopr2  10930  iseqf1olemkle  10934  iseqf1olemklt  10935  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemmo  10942  iseqf1olemqk  10944  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  seq3f1olemstep  10951  seq3f1oleml  10953  seq3f1o  10954  seqf1oglem2a  10955  seqf1oglem1  10956  seqf1oglem2  10957  seq3z  10965  seq3distr  10969  ser3ge0  10973  ser3le  10974  exp3vallem  10977  exp3val  10978  bcval5  11201  hashfz1  11222  resunimafz0  11274  leisorel  11289  zfz1isolemiso  11291  seq3coll  11294  ccatcl  11361  swrdclg  11422  caucvgrelemcau  11746  caucvgre  11747  cvg1nlemf  11749  cvg1nlemcau  11750  cvg1nlemres  11751  recvguniqlem  11760  resqrexlemdecn  11778  resqrexlemcalc3  11782  resqrexlemnmsq  11783  resqrexlemnm  11784  resqrexlemcvg  11785  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemga  11789  clim2ser  12103  clim2ser2  12104  climrecvg1n  12114  climcvg1nlem  12115  serf0  12118  sumeq2  12125  fsum3cvg  12145  summodclem2a  12148  fsum3  12154  fisumss  12159  fsumcl2lem  12165  fsumadd  12173  fsummulc2  12215  fsumrelem  12238  isumshft  12257  cvgratnnlemseq  12293  cvgratnnlemrate  12297  clim2prod  12306  clim2divap  12307  prodfrecap  12313  prodfdivap  12314  ntrivcvgap  12315  prodeq2  12324  fproddccvg  12339  prodmodclem3  12342  prodmodclem2a  12343  fprodseq  12350  fprodssdc  12357  fprodmul  12358  effsumlt  12459  nninfctlemfo  12817  nn0seqcvgd  12819  ialgrlem1st  12820  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  pcmpt2  13123  pcmptdvds  13124  1arithlem4  13145  1arith  13146  ennnfonelemdc  13290  ennnfonelemjn  13293  ennnfonelemg  13294  ennnfonelemp1  13297  ennnfonelemom  13299  ennnfonelemhdmp1  13300  ennnfonelemss  13301  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemnn0  13313  ennnfonelemim  13315  ctinfomlemom  13318  ctiunctlemudc  13328  ctiunctlemf  13329  ctiunctlemfo  13330  ssnnctlemct  13337  nninfdclemp1  13341  nninfdclemlt  13342  imasmnd2  13759  mhmf1o  13777  mhmco  13797  gzsumcl  13804  isgrpinv  13859  imasgrp2  13913  mhmid  13918  mhmmnd  13919  ghmgrp  13921  mulgval  13925  mulgfng  13927  mulgnnsubcl  13937  ghmid  14052  ghminv  14053  ghmmulg  14059  ghmnsgpreima  14072  ghmeqker  14074  ghmf1  14076  kerf1ghm  14077  ghmf1o  14078  gzsumsplit0  14148  gsumvalfi  14152  gsumclfi  14159  gsumsubmclfi  14163  pwssub  14216  imasring  14369  rhmopp  14483  lspcl  14728  znidomb  14993  znrrg  14995  asclelbas  15026  psrbaglesuppg  15057  psrbagfi  15059  psrbaglecl  15060  psrbagcon  15062  mplsubgfilemcl  15090  iscnp4  15319  cnptopco  15323  lmtopcnp  15351  upxp  15373  uptx  15375  txlm  15380  comet  15600  metcnp3  15612  metcnp  15613  metcnp2  15614  metcnpi3  15618  elcncf2  15675  cncfco  15692  ivthreinc  15746  limcimolemlt  15765  cnplimcim  15768  cnplimclemle  15769  cnplimclemr  15770  limccnpcntop  15776  dvlemap  15781  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvef  15828  plyaddlem1  15848  plymullem1  15849  plycoeid3  15858  plycolemc  15859  plycjlemc  15861  plycj  15862  plycn  15863  plyrecj  15864  dvply1  15866  dvply2g  15867  logfac  15995  lgsval  16123  lgscllem  16126  lgsval2lem  16129  lgsval4a  16141  lgsneg  16143  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgseisenlem3  16191  lgseisenlem4  16192  p1evtxdeqfi  16553  wlkvtxm  16581  wlkvtxiedg  16586  wlkvtxiedgg  16587  upgriswlkdc  16601  trlsegvdeglem7  16707  trlsegvdegfi  16708  eupth2lem3lem1fi  16709  eupth2lem3lem2fi  16710  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  eupth2lem3lem7fi  16715  eupth2lemsfi  16719  3dom  17018  pwle2  17028  subctctexmid  17030  nnsf  17048  peano4nninf  17049  nninfalllem1  17051  nninfsellemdc  17053  nninfsellemeq  17057  nninfsellemqall  17058  nninfsellemeqinf  17059  nninfomnilem  17061  nnnninfex  17065  nninfnfiinf  17066  repiecelem  17074  repiecele0  17075  repiecege0  17076  isomninnlem  17079  trilpolemeq1  17089  trilpolemlt1  17090  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102  nconstwlpolemgt0  17114  nconstwlpolem  17115