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  7319  supisoti  7351  ordiso2  7376  updjudhcoinlf  7421  updjudhcoinrg  7422  caseinl  7432  caseinr  7433  difinfsnlem  7440  difinfsn  7441  ctmlemr  7449  ctssdclemn0  7451  ctssdc  7454  enumctlemm  7455  enumct  7456  nnnninfeq2  7470  nninfisol  7474  enomnilem  7479  finomni  7481  ismkvnex  7496  enmkvlem  7502  enwomnilem  7510  nninfwlpoimlemg  7516  nninfwlpoimlemginf  7517  pr2cv1  7542  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  acnccim  7639  cauappcvgprlemm  8013  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlem2  8028  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgprlem2  8048  caucvgprprlemnkltj  8057  caucvgprprlemnkeqj  8058  caucvgprprlemnbj  8061  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  caucvgprprlemexb  8075  caucvgprprlemaddq  8076  caucvgprprlem1  8077  caucvgprprlem2  8078  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  caucvgsr  8170  axcaucvglemval  8265  axcaucvglemcau  8266  axcaucvglemres  8267  fseq1p1m1  10512  4fvwrd4  10558  fvinim0ffz  10671  frecuzrdgg  10868  frecuzrdgsuctlem  10875  seq3val  10912  seqvalcd  10913  seq3p1  10917  seqp1cd  10922  ser3mono  10939  seq3split  10940  seq3caopr2  10945  iseqf1olemkle  10949  iseqf1olemklt  10950  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemmo  10957  iseqf1olemqk  10959  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seq3f1olemstep  10966  seq3f1oleml  10968  seq3f1o  10969  seqf1oglem2a  10970  seqf1oglem1  10971  seqf1oglem2  10972  seq3z  10980  seq3distr  10984  ser3ge0  10988  ser3le  10989  exp3vallem  10992  exp3val  10993  bcval5  11217  hashfz1  11238  resunimafz0  11290  leisorel  11305  zfz1isolemiso  11307  seq3coll  11310  ccatcl  11377  swrdclg  11438  caucvgrelemcau  11762  caucvgre  11763  cvg1nlemf  11765  cvg1nlemcau  11766  cvg1nlemres  11767  recvguniqlem  11776  resqrexlemdecn  11794  resqrexlemcalc3  11798  resqrexlemnmsq  11799  resqrexlemnm  11800  resqrexlemcvg  11801  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemga  11805  fiidxsupcl  12012  clim2ser  12122  clim2ser2  12123  climrecvg1n  12133  climcvg1nlem  12134  serf0  12137  sumeq2  12144  fsum3cvg  12164  summodclem2a  12167  fsum3  12173  fisumss  12178  fsumcl2lem  12184  fsumadd  12192  fsummulc2  12234  fsumrelem  12257  isumshft  12276  cvgratnnlemseq  12312  cvgratnnlemrate  12316  clim2prod  12325  clim2divap  12326  prodfrecap  12332  prodfdivap  12333  ntrivcvgap  12334  prodeq2  12343  fproddccvg  12358  prodmodclem3  12361  prodmodclem2a  12362  fprodseq  12369  fprodssdc  12376  fprodmul  12377  effsumlt  12478  nninfctlemfo  12836  nn0seqcvgd  12838  ialgrlem1st  12839  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemh  13032  pcmpt2  13146  pcmptdvds  13147  1arithlem4  13168  1arith  13169  ennnfonelemdc  13342  ennnfonelemjn  13345  ennnfonelemg  13346  ennnfonelemp1  13349  ennnfonelemom  13351  ennnfonelemhdmp1  13352  ennnfonelemss  13353  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemnn0  13365  ennnfonelemim  13367  ctinfomlemom  13370  ctiunctlemudc  13380  ctiunctlemf  13381  ctiunctlemfo  13382  ssnnctlemct  13389  nninfdclemp1  13393  nninfdclemlt  13394  imasmnd2  13812  mhmf1o  13830  mhmco  13850  gzsumcl  13857  isgrpinv  13912  imasgrp2  13966  mhmid  13971  mhmmnd  13972  ghmgrp  13974  mulgval  13978  mulgfng  13980  mulgnnsubcl  13990  ghmid  14105  ghminv  14106  ghmmulg  14112  ghmnsgpreima  14125  ghmeqker  14127  ghmf1  14129  kerf1ghm  14130  ghmf1o  14131  gzsumsplit0  14232  gsumvalfi  14236  gsumclfi  14243  gsumsubmclfi  14247  pwssub  14300  imasring  14453  rhmopp  14567  lspcl  14812  znidomb  15077  znrrg  15079  asclelbas  15110  psrbaglesuppg  15141  psrbagfi  15143  psrbaglecl  15144  psrbagcon  15146  psrbaglefifi  15147  rhmpsrfilem2  15157  psrmulvalfi  15160  mplsubgfilemcl  15181  iscnp4  15410  cnptopco  15414  lmtopcnp  15442  upxp  15464  uptx  15466  txlm  15471  comet  15691  metcnp3  15703  metcnp  15704  metcnp2  15705  metcnpi3  15709  elcncf2  15766  cncfco  15783  ivthreinc  15837  limcimolemlt  15856  cnplimcim  15859  cnplimclemle  15860  cnplimclemr  15861  limccnpcntop  15867  dvlemap  15872  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvef  15919  plyaddlem1  15939  plymullem1  15940  plycoeid3  15949  plycolemc  15950  plycjlemc  15952  plycj  15953  plycn  15954  plyrecj  15955  dvply1  15957  dvply2g  15958  logfac  16090  bposlem3  16274  bposlem5  16276  bposlem6  16277  bposlem9  16280  lgsval  16289  lgscllem  16292  lgsval2lem  16295  lgsval4a  16307  lgsneg  16309  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  lgseisenlem3  16357  lgseisenlem4  16358  p1evtxdeqfi  16719  wlkvtxm  16747  wlkvtxiedg  16752  wlkvtxiedgg  16753  upgriswlkdc  16767  trlsegvdeglem7  16873  trlsegvdegfi  16874  eupth2lem3lem1fi  16875  eupth2lem3lem2fi  16876  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880  eupth2lem3lem7fi  16881  eupth2lemsfi  16885  3dom  17184  pwle2  17194  subctctexmid  17196  nnsf  17214  peano4nninf  17215  nninfalllem1  17217  nninfsellemdc  17219  nninfsellemeq  17223  nninfsellemqall  17224  nninfsellemeqinf  17225  nninfomnilem  17227  nnnninfex  17231  nninfnfiinf  17232  repiecelem  17240  repiecele0  17241  repiecege0  17242  isomninnlem  17245  trilpolemeq1  17256  trilpolemlt1  17257  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269  nconstwlpolemgt0  17281  nconstwlpolem  17282