Theorem ffvelcdmd 5773

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypotheses

Ref	Expression
ffvelcdmd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
ffvelcdmd.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
ffvelcdmd	⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelcdmd

Step	Hyp	Ref	Expression
1		ffvelcdmd.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		ffvelcdmd.1	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
3	2	ffvelcdmda 5772	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
4	1, 3	mpdan 421	1 ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2200  ⟶wf 5314  ‘cfv 5318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-fv 5326

This theorem is referenced by:  isotr  5946  caofinvl  6250  rdgon  6538  frecabcl  6551  phplem4dom  7031  fidceq  7039  dif1en  7049  fin0  7055  fin0or  7056  infm  7077  en2eqpr  7080  fidcenumlemrks  7131  fidcenumlemr  7133  supisoti  7188  ordiso2  7213  updjudhcoinlf  7258  updjudhcoinrg  7259  caseinl  7269  caseinr  7270  difinfsnlem  7277  difinfsn  7278  ctmlemr  7286  ctssdclemn0  7288  ctssdc  7291  enumctlemm  7292  enumct  7293  nnnninfeq2  7307  nninfisol  7311  enomnilem  7316  finomni  7318  ismkvnex  7333  enmkvlem  7339  enwomnilem  7347  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  pr2cv1  7379  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acnccim  7469  cauappcvgprlemm  7843  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfu  7852  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnbj  7891  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemloc  7901  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  caucvgprprlemaddq  7906  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  caucvgsr  8000  axcaucvglemval  8095  axcaucvglemcau  8096  axcaucvglemres  8097  fseq1p1m1  10302  4fvwrd4  10348  fvinim0ffz  10459  frecuzrdgg  10650  frecuzrdgsuctlem  10657  seq3val  10694  seqvalcd  10695  seq3p1  10699  seqp1cd  10704  ser3mono  10721  seq3split  10722  seq3caopr2  10727  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemmo  10739  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1olemstep  10748  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem2a  10752  seqf1oglem1  10753  seqf1oglem2  10754  seq3z  10762  seq3distr  10766  ser3ge0  10770  ser3le  10771  exp3vallem  10774  exp3val  10775  bcval5  10997  hashfz1  11017  resunimafz0  11066  leisorel  11072  zfz1isolemiso  11074  seq3coll  11077  ccatcl  11141  swrdclg  11198  caucvgrelemcau  11507  caucvgre  11508  cvg1nlemf  11510  cvg1nlemcau  11511  cvg1nlemres  11512  recvguniqlem  11521  resqrexlemdecn  11539  resqrexlemcalc3  11543  resqrexlemnmsq  11544  resqrexlemnm  11545  resqrexlemcvg  11546  resqrexlemoverl  11548  resqrexlemglsq  11549  resqrexlemga  11550  clim2ser  11864  clim2ser2  11865  climrecvg1n  11875  climcvg1nlem  11876  serf0  11879  sumeq2  11886  fsum3cvg  11905  summodclem2a  11908  fsum3  11914  fisumss  11919  fsumcl2lem  11925  fsumadd  11933  fsummulc2  11975  fsumrelem  11998  isumshft  12017  cvgratnnlemseq  12053  cvgratnnlemrate  12057  clim2prod  12066  clim2divap  12067  prodfrecap  12073  prodfdivap  12074  ntrivcvgap  12075  prodeq2  12084  fproddccvg  12099  prodmodclem3  12102  prodmodclem2a  12103  fprodseq  12110  fprodssdc  12117  fprodmul  12118  effsumlt  12219  nninfctlemfo  12577  nn0seqcvgd  12579  ialgrlem1st  12580  eulerthlemrprm  12767  eulerthlema  12768  eulerthlemh  12769  pcmpt2  12883  pcmptdvds  12884  1arithlem4  12905  1arith  12906  ennnfonelemdc  12986  ennnfonelemjn  12989  ennnfonelemg  12990  ennnfonelemp1  12993  ennnfonelemom  12995  ennnfonelemhdmp1  12996  ennnfonelemss  12997  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemnn0  13009  ennnfonelemim  13011  ctinfomlemom  13014  ctiunctlemudc  13024  ctiunctlemf  13025  ctiunctlemfo  13026  ssnnctlemct  13033  nninfdclemp1  13037  nninfdclemlt  13038  imasmnd2  13501  mhmf1o  13519  mhmco  13539  gsumfzcl  13548  isgrpinv  13603  pwssub  13662  imasgrp2  13663  mhmid  13668  mhmmnd  13669  ghmgrp  13671  mulgval  13675  mulgfng  13677  mulgnnsubcl  13687  ghmid  13802  ghminv  13803  ghmmulg  13809  ghmnsgpreima  13822  ghmeqker  13824  ghmf1  13826  kerf1ghm  13827  ghmf1o  13828  imasring  14043  rhmopp  14156  lspcl  14371  znidomb  14638  znrrg  14640  psrbaglesuppg  14652  psrbagfi  14653  mplsubgfilemcl  14679  iscnp4  14908  cnptopco  14912  lmtopcnp  14940  upxp  14962  uptx  14964  txlm  14969  comet  15189  metcnp3  15201  metcnp  15202  metcnp2  15203  metcnpi3  15207  elcncf2  15264  cncfco  15281  ivthreinc  15335  limcimolemlt  15354  cnplimcim  15357  cnplimclemle  15358  cnplimclemr  15359  limccnpcntop  15365  dvlemap  15370  dvcnp2cntop  15389  dvaddxxbr  15391  dvmulxxbr  15392  dvcoapbr  15397  dvcjbr  15398  dvef  15417  plyaddlem1  15437  plymullem1  15438  plycoeid3  15447  plycolemc  15448  plycjlemc  15450  plycj  15451  plycn  15452  plyrecj  15453  dvply1  15455  dvply2g  15456  lgsval  15699  lgscllem  15702  lgsval2lem  15705  lgsval4a  15717  lgsneg  15719  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  lgseisenlem3  15767  lgseisenlem4  15768  wlkvtxm  16086  wlkvtxiedg  16091  wlkvtxiedgg  16092  upgriswlkdc  16106  1dom1el  16437  3dom  16439  2omap  16446  pwle2  16451  subctctexmid  16453  nnsf  16459  peano4nninf  16460  nninfalllem1  16462  nninfsellemdc  16464  nninfsellemeq  16468  nninfsellemqall  16469  nninfsellemeqinf  16470  nninfomnilem  16472  nnnninfex  16476  nninfnfiinf  16477  isomninnlem  16486  trilpolemeq1  16496  trilpolemlt1  16497  iswomninnlem  16505  iswomni0  16507  ismkvnnlem  16508  nconstwlpolemgt0  16520  nconstwlpolem  16521