Theorem ffvelcdmd 5779

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 5778	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
4	1, 3	mpdan 421	1 ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2200  ⟶wf 5320  ‘cfv 5324

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 4205  ax-pow 4262  ax-pr 4297

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 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-fv 5332

This theorem is referenced by:  isotr  5952  caofinvl  6256  rdgon  6547  frecabcl  6560  1dom1el  6988  phplem4dom  7043  fidceq  7051  dif1en  7063  fin0  7069  fin0or  7070  infm  7091  en2eqpr  7094  fidcenumlemrks  7146  fidcenumlemr  7148  supisoti  7203  ordiso2  7228  updjudhcoinlf  7273  updjudhcoinrg  7274  caseinl  7284  caseinr  7285  difinfsnlem  7292  difinfsn  7293  ctmlemr  7301  ctssdclemn0  7303  ctssdc  7306  enumctlemm  7307  enumct  7308  nnnninfeq2  7322  nninfisol  7326  enomnilem  7331  finomni  7333  ismkvnex  7348  enmkvlem  7354  enwomnilem  7362  nninfwlpoimlemg  7368  nninfwlpoimlemginf  7369  pr2cv1  7394  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  acnccim  7484  cauappcvgprlemm  7858  cauappcvgprlemdisj  7864  cauappcvgprlemloc  7865  cauappcvgprlemladdfu  7867  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  cauappcvgprlem1  7872  cauappcvgprlem2  7873  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprlemm  7881  caucvgprlemloc  7888  caucvgprlemladdfu  7890  caucvgprlemladdrl  7891  caucvgprlem1  7892  caucvgprlem2  7893  caucvgprprlemnkltj  7902  caucvgprprlemnkeqj  7903  caucvgprprlemnbj  7906  caucvgprprlemmu  7908  caucvgprprlemopl  7910  caucvgprprlemloc  7916  caucvgprprlemexbt  7919  caucvgprprlemexb  7920  caucvgprprlemaddq  7921  caucvgprprlem1  7922  caucvgprprlem2  7923  caucvgsrlemcau  8006  caucvgsrlemgt1  8008  caucvgsrlemoffcau  8011  caucvgsrlemoffres  8013  caucvgsr  8015  axcaucvglemval  8110  axcaucvglemcau  8111  axcaucvglemres  8112  fseq1p1m1  10322  4fvwrd4  10368  fvinim0ffz  10480  frecuzrdgg  10671  frecuzrdgsuctlem  10678  seq3val  10715  seqvalcd  10716  seq3p1  10720  seqp1cd  10725  ser3mono  10742  seq3split  10743  seq3caopr2  10748  iseqf1olemkle  10752  iseqf1olemklt  10753  iseqf1olemqcl  10754  iseqf1olemnab  10756  iseqf1olemmo  10760  iseqf1olemqk  10762  iseqf1olemjpcl  10763  iseqf1olemqpcl  10764  iseqf1olemfvp  10765  seq3f1olemqsumkj  10766  seq3f1olemqsumk  10767  seq3f1olemqsum  10768  seq3f1olemstep  10769  seq3f1oleml  10771  seq3f1o  10772  seqf1oglem2a  10773  seqf1oglem1  10774  seqf1oglem2  10775  seq3z  10783  seq3distr  10787  ser3ge0  10791  ser3le  10792  exp3vallem  10795  exp3val  10796  bcval5  11018  hashfz1  11038  resunimafz0  11088  leisorel  11094  zfz1isolemiso  11096  seq3coll  11099  ccatcl  11163  swrdclg  11224  caucvgrelemcau  11534  caucvgre  11535  cvg1nlemf  11537  cvg1nlemcau  11538  cvg1nlemres  11539  recvguniqlem  11548  resqrexlemdecn  11566  resqrexlemcalc3  11570  resqrexlemnmsq  11571  resqrexlemnm  11572  resqrexlemcvg  11573  resqrexlemoverl  11575  resqrexlemglsq  11576  resqrexlemga  11577  clim2ser  11891  clim2ser2  11892  climrecvg1n  11902  climcvg1nlem  11903  serf0  11906  sumeq2  11913  fsum3cvg  11932  summodclem2a  11935  fsum3  11941  fisumss  11946  fsumcl2lem  11952  fsumadd  11960  fsummulc2  12002  fsumrelem  12025  isumshft  12044  cvgratnnlemseq  12080  cvgratnnlemrate  12084  clim2prod  12093  clim2divap  12094  prodfrecap  12100  prodfdivap  12101  ntrivcvgap  12102  prodeq2  12111  fproddccvg  12126  prodmodclem3  12129  prodmodclem2a  12130  fprodseq  12137  fprodssdc  12144  fprodmul  12145  effsumlt  12246  nninfctlemfo  12604  nn0seqcvgd  12606  ialgrlem1st  12607  eulerthlemrprm  12794  eulerthlema  12795  eulerthlemh  12796  pcmpt2  12910  pcmptdvds  12911  1arithlem4  12932  1arith  12933  ennnfonelemdc  13013  ennnfonelemjn  13016  ennnfonelemg  13017  ennnfonelemp1  13020  ennnfonelemom  13022  ennnfonelemhdmp1  13023  ennnfonelemss  13024  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemex  13028  ennnfonelemhom  13029  ennnfonelemnn0  13036  ennnfonelemim  13038  ctinfomlemom  13041  ctiunctlemudc  13051  ctiunctlemf  13052  ctiunctlemfo  13053  ssnnctlemct  13060  nninfdclemp1  13064  nninfdclemlt  13065  imasmnd2  13528  mhmf1o  13546  mhmco  13566  gsumfzcl  13575  isgrpinv  13630  pwssub  13689  imasgrp2  13690  mhmid  13695  mhmmnd  13696  ghmgrp  13698  mulgval  13702  mulgfng  13704  mulgnnsubcl  13714  ghmid  13829  ghminv  13830  ghmmulg  13836  ghmnsgpreima  13849  ghmeqker  13851  ghmf1  13853  kerf1ghm  13854  ghmf1o  13855  imasring  14070  rhmopp  14183  lspcl  14398  znidomb  14665  znrrg  14667  psrbaglesuppg  14679  psrbagfi  14680  mplsubgfilemcl  14706  iscnp4  14935  cnptopco  14939  lmtopcnp  14967  upxp  14989  uptx  14991  txlm  14996  comet  15216  metcnp3  15228  metcnp  15229  metcnp2  15230  metcnpi3  15234  elcncf2  15291  cncfco  15308  ivthreinc  15362  limcimolemlt  15381  cnplimcim  15384  cnplimclemle  15385  cnplimclemr  15386  limccnpcntop  15392  dvlemap  15397  dvcnp2cntop  15416  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  dvcjbr  15425  dvef  15444  plyaddlem1  15464  plymullem1  15465  plycoeid3  15474  plycolemc  15475  plycjlemc  15477  plycj  15478  plycn  15479  plyrecj  15480  dvply1  15482  dvply2g  15483  lgsval  15726  lgscllem  15729  lgsval2lem  15732  lgsval4a  15744  lgsneg  15746  lgsdir  15757  lgsdilem2  15758  lgsdi  15759  lgsne0  15760  lgseisenlem3  15794  lgseisenlem4  15795  p1evtxdeqfi  16123  wlkvtxm  16151  wlkvtxiedg  16156  wlkvtxiedgg  16157  upgriswlkdc  16171  3dom  16537  2omap  16544  pwle2  16549  subctctexmid  16551  nnsf  16557  peano4nninf  16558  nninfalllem1  16560  nninfsellemdc  16562  nninfsellemeq  16566  nninfsellemqall  16567  nninfsellemeqinf  16568  nninfomnilem  16570  nnnninfex  16574  nninfnfiinf  16575  isomninnlem  16584  trilpolemeq1  16594  trilpolemlt1  16595  iswomninnlem  16603  iswomni0  16605  ismkvnnlem  16606  nconstwlpolemgt0  16618  nconstwlpolem  16619  gfsumval  16630