Theorem ffvelcdmd 5838

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

Syntax hints:   → wi 4   ∈ wcel 2209  ⟶wf 5371  ‘cfv 5375

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 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 4247  ax-pow 4309  ax-pr 4344

This theorem 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 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-fv 5383

This theorem is referenced by:  isotr  6016  caofinvl  6322  fvdifsuppst  6478  rdgon  6651  frecabcl  6664  1dom1el  7101  phplem4dom  7157  fidceq  7165  dif1en  7177  fin0  7183  fin0or  7184  infm  7205  en2eqpr  7208  fidcenumlemrks  7264  fidcenumlemr  7266  fdcf1  7310  2omap  7312  supisoti  7344  ordiso2  7369  updjudhcoinlf  7414  updjudhcoinrg  7415  caseinl  7425  caseinr  7426  difinfsnlem  7433  difinfsn  7434  ctmlemr  7442  ctssdclemn0  7444  ctssdc  7447  enumctlemm  7448  enumct  7449  nnnninfeq2  7463  nninfisol  7467  enomnilem  7472  finomni  7474  ismkvnex  7489  enmkvlem  7495  enwomnilem  7503  nninfwlpoimlemg  7509  nninfwlpoimlemginf  7510  pr2cv1  7535  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  acnccim  7632  cauappcvgprlemm  8006  cauappcvgprlemdisj  8012  cauappcvgprlemloc  8013  cauappcvgprlemladdfu  8015  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  cauappcvgprlem1  8020  cauappcvgprlem2  8021  caucvgprlemnkj  8027  caucvgprlemnbj  8028  caucvgprlemm  8029  caucvgprlemloc  8036  caucvgprlemladdfu  8038  caucvgprlemladdrl  8039  caucvgprlem1  8040  caucvgprlem2  8041  caucvgprprlemnkltj  8050  caucvgprprlemnkeqj  8051  caucvgprprlemnbj  8054  caucvgprprlemmu  8056  caucvgprprlemopl  8058  caucvgprprlemloc  8064  caucvgprprlemexbt  8067  caucvgprprlemexb  8068  caucvgprprlemaddq  8069  caucvgprprlem1  8070  caucvgprprlem2  8071  caucvgsrlemcau  8154  caucvgsrlemgt1  8156  caucvgsrlemoffcau  8159  caucvgsrlemoffres  8161  caucvgsr  8163  axcaucvglemval  8258  axcaucvglemcau  8259  axcaucvglemres  8260  fseq1p1m1  10484  4fvwrd4  10530  fvinim0ffz  10643  frecuzrdgg  10836  frecuzrdgsuctlem  10843  seq3val  10880  seqvalcd  10881  seq3p1  10885  seqp1cd  10890  ser3mono  10907  seq3split  10908  seq3caopr2  10913  iseqf1olemkle  10917  iseqf1olemklt  10918  iseqf1olemqcl  10919  iseqf1olemnab  10921  iseqf1olemmo  10925  iseqf1olemqk  10927  iseqf1olemjpcl  10928  iseqf1olemqpcl  10929  iseqf1olemfvp  10930  seq3f1olemqsumkj  10931  seq3f1olemqsumk  10932  seq3f1olemqsum  10933  seq3f1olemstep  10934  seq3f1oleml  10936  seq3f1o  10937  seqf1oglem2a  10938  seqf1oglem1  10939  seqf1oglem2  10940  seq3z  10948  seq3distr  10952  ser3ge0  10956  ser3le  10957  exp3vallem  10960  exp3val  10961  bcval5  11184  hashfz1  11205  resunimafz0  11257  leisorel  11272  zfz1isolemiso  11274  seq3coll  11277  ccatcl  11344  swrdclg  11405  caucvgrelemcau  11729  caucvgre  11730  cvg1nlemf  11732  cvg1nlemcau  11733  cvg1nlemres  11734  recvguniqlem  11743  resqrexlemdecn  11761  resqrexlemcalc3  11765  resqrexlemnmsq  11766  resqrexlemnm  11767  resqrexlemcvg  11768  resqrexlemoverl  11770  resqrexlemglsq  11771  resqrexlemga  11772  clim2ser  12086  clim2ser2  12087  climrecvg1n  12097  climcvg1nlem  12098  serf0  12101  sumeq2  12108  fsum3cvg  12128  summodclem2a  12131  fsum3  12137  fisumss  12142  fsumcl2lem  12148  fsumadd  12156  fsummulc2  12198  fsumrelem  12221  isumshft  12240  cvgratnnlemseq  12276  cvgratnnlemrate  12280  clim2prod  12289  clim2divap  12290  prodfrecap  12296  prodfdivap  12297  ntrivcvgap  12298  prodeq2  12307  fproddccvg  12322  prodmodclem3  12325  prodmodclem2a  12326  fprodseq  12333  fprodssdc  12340  fprodmul  12341  effsumlt  12442  nninfctlemfo  12800  nn0seqcvgd  12802  ialgrlem1st  12803  eulerthlemrprm  12990  eulerthlema  12991  eulerthlemh  12992  pcmpt2  13106  pcmptdvds  13107  1arithlem4  13128  1arith  13129  ennnfonelemdc  13273  ennnfonelemjn  13276  ennnfonelemg  13277  ennnfonelemp1  13280  ennnfonelemom  13282  ennnfonelemhdmp1  13283  ennnfonelemss  13284  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemex  13288  ennnfonelemhom  13289  ennnfonelemnn0  13296  ennnfonelemim  13298  ctinfomlemom  13301  ctiunctlemudc  13311  ctiunctlemf  13312  ctiunctlemfo  13313  ssnnctlemct  13320  nninfdclemp1  13324  nninfdclemlt  13325  imasmnd2  13742  mhmf1o  13760  mhmco  13780  gzsumcl  13787  isgrpinv  13842  imasgrp2  13896  mhmid  13901  mhmmnd  13902  ghmgrp  13904  mulgval  13908  mulgfng  13910  mulgnnsubcl  13920  ghmid  14035  ghminv  14036  ghmmulg  14042  ghmnsgpreima  14055  ghmeqker  14057  ghmf1  14059  kerf1ghm  14060  ghmf1o  14061  gzsumsplit0  14131  gsumvalfi  14135  gsumclfi  14142  gsumsubmclfi  14146  pwssub  14199  imasring  14352  rhmopp  14466  lspcl  14711  znidomb  14976  znrrg  14978  asclelbas  15009  psrbaglesuppg  15040  psrbagfi  15042  psrbaglecl  15043  psrbagcon  15045  mplsubgfilemcl  15073  iscnp4  15302  cnptopco  15306  lmtopcnp  15334  upxp  15356  uptx  15358  txlm  15363  comet  15583  metcnp3  15595  metcnp  15596  metcnp2  15597  metcnpi3  15601  elcncf2  15658  cncfco  15675  ivthreinc  15729  limcimolemlt  15748  cnplimcim  15751  cnplimclemle  15752  cnplimclemr  15753  limccnpcntop  15759  dvlemap  15764  dvcnp2cntop  15783  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  dvcjbr  15792  dvef  15811  plyaddlem1  15831  plymullem1  15832  plycoeid3  15841  plycolemc  15842  plycjlemc  15844  plycj  15845  plycn  15846  plyrecj  15847  dvply1  15849  dvply2g  15850  logfac  15978  lgsval  16106  lgscllem  16109  lgsval2lem  16112  lgsval4a  16124  lgsneg  16126  lgsdir  16137  lgsdilem2  16138  lgsdi  16139  lgsne0  16140  lgseisenlem3  16174  lgseisenlem4  16175  p1evtxdeqfi  16536  wlkvtxm  16564  wlkvtxiedg  16569  wlkvtxiedgg  16570  upgriswlkdc  16584  trlsegvdeglem7  16690  trlsegvdegfi  16691  eupth2lem3lem1fi  16692  eupth2lem3lem2fi  16693  eupth2lem3lem3fi  16694  eupth2lem3lem6fi  16695  eupth2lem3lem4fi  16697  eupth2lem3lem7fi  16698  eupth2lemsfi  16702  3dom  17001  pwle2  17011  subctctexmid  17013  nnsf  17022  peano4nninf  17023  nninfalllem1  17025  nninfsellemdc  17027  nninfsellemeq  17031  nninfsellemqall  17032  nninfsellemeqinf  17033  nninfomnilem  17035  nnnninfex  17039  nninfnfiinf  17040  repiecelem  17048  repiecele0  17049  repiecege0  17050  isomninnlem  17053  trilpolemeq1  17063  trilpolemlt1  17064  iswomninnlem  17073  iswomni0  17075  ismkvnnlem  17076  nconstwlpolemgt0  17088  nconstwlpolem  17089