Theorem ffvelcdmd 5783

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

Syntax hints:   → wi 4   ∈ wcel 2202  ⟶wf 5322  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334

This theorem is referenced by:  isotr  5957  caofinvl  6261  rdgon  6552  frecabcl  6565  1dom1el  6993  phplem4dom  7048  fidceq  7056  dif1en  7068  fin0  7074  fin0or  7075  infm  7096  en2eqpr  7099  fidcenumlemrks  7152  fidcenumlemr  7154  supisoti  7209  ordiso2  7234  updjudhcoinlf  7279  updjudhcoinrg  7280  caseinl  7290  caseinr  7291  difinfsnlem  7298  difinfsn  7299  ctmlemr  7307  ctssdclemn0  7309  ctssdc  7312  enumctlemm  7313  enumct  7314  nnnninfeq2  7328  nninfisol  7332  enomnilem  7337  finomni  7339  ismkvnex  7354  enmkvlem  7360  enwomnilem  7368  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  pr2cv1  7400  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acnccim  7491  cauappcvgprlemm  7865  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprlem2  7900  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnbj  7913  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  caucvgprprlemaddq  7928  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  caucvgsr  8022  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  fseq1p1m1  10329  4fvwrd4  10375  fvinim0ffz  10488  frecuzrdgg  10679  frecuzrdgsuctlem  10686  seq3val  10723  seqvalcd  10724  seq3p1  10728  seqp1cd  10733  ser3mono  10750  seq3split  10751  seq3caopr2  10756  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemmo  10768  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem2a  10781  seqf1oglem1  10782  seqf1oglem2  10783  seq3z  10791  seq3distr  10795  ser3ge0  10799  ser3le  10800  exp3vallem  10803  exp3val  10804  bcval5  11026  hashfz1  11046  resunimafz0  11096  leisorel  11102  zfz1isolemiso  11104  seq3coll  11107  ccatcl  11171  swrdclg  11232  caucvgrelemcau  11542  caucvgre  11543  cvg1nlemf  11545  cvg1nlemcau  11546  cvg1nlemres  11547  recvguniqlem  11556  resqrexlemdecn  11574  resqrexlemcalc3  11578  resqrexlemnmsq  11579  resqrexlemnm  11580  resqrexlemcvg  11581  resqrexlemoverl  11583  resqrexlemglsq  11584  resqrexlemga  11585  clim2ser  11899  clim2ser2  11900  climrecvg1n  11910  climcvg1nlem  11911  serf0  11914  sumeq2  11921  fsum3cvg  11941  summodclem2a  11944  fsum3  11950  fisumss  11955  fsumcl2lem  11961  fsumadd  11969  fsummulc2  12011  fsumrelem  12034  isumshft  12053  cvgratnnlemseq  12089  cvgratnnlemrate  12093  clim2prod  12102  clim2divap  12103  prodfrecap  12109  prodfdivap  12110  ntrivcvgap  12111  prodeq2  12120  fproddccvg  12135  prodmodclem3  12138  prodmodclem2a  12139  fprodseq  12146  fprodssdc  12153  fprodmul  12154  effsumlt  12255  nninfctlemfo  12613  nn0seqcvgd  12615  ialgrlem1st  12616  eulerthlemrprm  12803  eulerthlema  12804  eulerthlemh  12805  pcmpt2  12919  pcmptdvds  12920  1arithlem4  12941  1arith  12942  ennnfonelemdc  13022  ennnfonelemjn  13025  ennnfonelemg  13026  ennnfonelemp1  13029  ennnfonelemom  13031  ennnfonelemhdmp1  13032  ennnfonelemss  13033  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemex  13037  ennnfonelemhom  13038  ennnfonelemnn0  13045  ennnfonelemim  13047  ctinfomlemom  13050  ctiunctlemudc  13060  ctiunctlemf  13061  ctiunctlemfo  13062  ssnnctlemct  13069  nninfdclemp1  13073  nninfdclemlt  13074  imasmnd2  13537  mhmf1o  13555  mhmco  13575  gsumfzcl  13584  isgrpinv  13639  pwssub  13698  imasgrp2  13699  mhmid  13704  mhmmnd  13705  ghmgrp  13707  mulgval  13711  mulgfng  13713  mulgnnsubcl  13723  ghmid  13838  ghminv  13839  ghmmulg  13845  ghmnsgpreima  13858  ghmeqker  13860  ghmf1  13862  kerf1ghm  13863  ghmf1o  13864  gsumsplit0  13935  imasring  14080  rhmopp  14193  lspcl  14408  znidomb  14675  znrrg  14677  psrbaglesuppg  14689  psrbagfi  14690  mplsubgfilemcl  14716  iscnp4  14945  cnptopco  14949  lmtopcnp  14977  upxp  14999  uptx  15001  txlm  15006  comet  15226  metcnp3  15238  metcnp  15239  metcnp2  15240  metcnpi3  15244  elcncf2  15301  cncfco  15318  ivthreinc  15372  limcimolemlt  15391  cnplimcim  15394  cnplimclemle  15395  cnplimclemr  15396  limccnpcntop  15402  dvlemap  15407  dvcnp2cntop  15426  dvaddxxbr  15428  dvmulxxbr  15429  dvcoapbr  15434  dvcjbr  15435  dvef  15454  plyaddlem1  15474  plymullem1  15475  plycoeid3  15484  plycolemc  15485  plycjlemc  15487  plycj  15488  plycn  15489  plyrecj  15490  dvply1  15492  dvply2g  15493  lgsval  15736  lgscllem  15739  lgsval2lem  15742  lgsval4a  15754  lgsneg  15756  lgsdir  15767  lgsdilem2  15768  lgsdi  15769  lgsne0  15770  lgseisenlem3  15804  lgseisenlem4  15805  p1evtxdeqfi  16166  wlkvtxm  16194  wlkvtxiedg  16199  wlkvtxiedgg  16200  upgriswlkdc  16214  trlsegvdeglem7  16320  trlsegvdegfi  16321  eupth2lem3lem1fi  16322  eupth2lem3lem2fi  16323  eupth2lem3lem3fi  16324  eupth2lem3lem6fi  16325  eupth2lem3lem4fi  16327  eupth2lem3lem7fi  16328  eupth2lemsfi  16332  3dom  16608  2omap  16615  pwle2  16620  subctctexmid  16622  nnsf  16628  peano4nninf  16629  nninfalllem1  16631  nninfsellemdc  16633  nninfsellemeq  16637  nninfsellemqall  16638  nninfsellemeqinf  16639  nninfomnilem  16641  nnnninfex  16645  nninfnfiinf  16646  isomninnlem  16655  trilpolemeq1  16665  trilpolemlt1  16666  iswomninnlem  16674  iswomni0  16676  ismkvnnlem  16677  nconstwlpolemgt0  16689  nconstwlpolem  16690  gfsumval  16701  gfsumcl  16708