Theorem ffvelcdmd 5812

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

Syntax hints:   → wi 4   ∈ wcel 2203  ⟶wf 5347  ‘cfv 5351

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-sbc 3042  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-iota 5311  df-fun 5353  df-fn 5354  df-f 5355  df-fv 5359

This theorem is referenced by:  isotr  5988  caofinvl  6291  fvdifsuppst  6443  rdgon  6616  frecabcl  6629  1dom1el  7059  phplem4dom  7115  fidceq  7123  dif1en  7135  fin0  7141  fin0or  7142  infm  7163  en2eqpr  7166  fidcenumlemrks  7222  fidcenumlemr  7224  2omap  7268  supisoti  7300  ordiso2  7325  updjudhcoinlf  7370  updjudhcoinrg  7371  caseinl  7381  caseinr  7382  difinfsnlem  7389  difinfsn  7390  ctmlemr  7398  ctssdclemn0  7400  ctssdc  7403  enumctlemm  7404  enumct  7405  nnnninfeq2  7419  nninfisol  7423  enomnilem  7428  finomni  7430  ismkvnex  7445  enmkvlem  7451  enwomnilem  7459  nninfwlpoimlemg  7465  nninfwlpoimlemginf  7466  pr2cv1  7491  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  acnccim  7582  cauappcvgprlemm  7956  cauappcvgprlemdisj  7962  cauappcvgprlemloc  7963  cauappcvgprlemladdfu  7965  cauappcvgprlemladdru  7967  cauappcvgprlemladdrl  7968  cauappcvgprlem1  7970  cauappcvgprlem2  7971  caucvgprlemnkj  7977  caucvgprlemnbj  7978  caucvgprlemm  7979  caucvgprlemloc  7986  caucvgprlemladdfu  7988  caucvgprlemladdrl  7989  caucvgprlem1  7990  caucvgprlem2  7991  caucvgprprlemnkltj  8000  caucvgprprlemnkeqj  8001  caucvgprprlemnbj  8004  caucvgprprlemmu  8006  caucvgprprlemopl  8008  caucvgprprlemloc  8014  caucvgprprlemexbt  8017  caucvgprprlemexb  8018  caucvgprprlemaddq  8019  caucvgprprlem1  8020  caucvgprprlem2  8021  caucvgsrlemcau  8104  caucvgsrlemgt1  8106  caucvgsrlemoffcau  8109  caucvgsrlemoffres  8111  caucvgsr  8113  axcaucvglemval  8208  axcaucvglemcau  8209  axcaucvglemres  8210  fseq1p1m1  10424  4fvwrd4  10470  fvinim0ffz  10583  frecuzrdgg  10774  frecuzrdgsuctlem  10781  seq3val  10818  seqvalcd  10819  seq3p1  10823  seqp1cd  10828  ser3mono  10845  seq3split  10846  seq3caopr2  10851  iseqf1olemkle  10855  iseqf1olemklt  10856  iseqf1olemqcl  10857  iseqf1olemnab  10859  iseqf1olemmo  10863  iseqf1olemqk  10865  iseqf1olemjpcl  10866  iseqf1olemqpcl  10867  iseqf1olemfvp  10868  seq3f1olemqsumkj  10869  seq3f1olemqsumk  10870  seq3f1olemqsum  10871  seq3f1olemstep  10872  seq3f1oleml  10874  seq3f1o  10875  seqf1oglem2a  10876  seqf1oglem1  10877  seqf1oglem2  10878  seq3z  10886  seq3distr  10890  ser3ge0  10894  ser3le  10895  exp3vallem  10898  exp3val  10899  bcval5  11121  hashfz1  11141  resunimafz0  11191  leisorel  11202  zfz1isolemiso  11204  seq3coll  11207  ccatcl  11274  swrdclg  11335  caucvgrelemcau  11658  caucvgre  11659  cvg1nlemf  11661  cvg1nlemcau  11662  cvg1nlemres  11663  recvguniqlem  11672  resqrexlemdecn  11690  resqrexlemcalc3  11694  resqrexlemnmsq  11695  resqrexlemnm  11696  resqrexlemcvg  11697  resqrexlemoverl  11699  resqrexlemglsq  11700  resqrexlemga  11701  clim2ser  12015  clim2ser2  12016  climrecvg1n  12026  climcvg1nlem  12027  serf0  12030  sumeq2  12037  fsum3cvg  12057  summodclem2a  12060  fsum3  12066  fisumss  12071  fsumcl2lem  12077  fsumadd  12085  fsummulc2  12127  fsumrelem  12150  isumshft  12169  cvgratnnlemseq  12205  cvgratnnlemrate  12209  clim2prod  12218  clim2divap  12219  prodfrecap  12225  prodfdivap  12226  ntrivcvgap  12227  prodeq2  12236  fproddccvg  12251  prodmodclem3  12254  prodmodclem2a  12255  fprodseq  12262  fprodssdc  12269  fprodmul  12270  effsumlt  12371  nninfctlemfo  12729  nn0seqcvgd  12731  ialgrlem1st  12732  eulerthlemrprm  12919  eulerthlema  12920  eulerthlemh  12921  pcmpt2  13035  pcmptdvds  13036  1arithlem4  13057  1arith  13058  ennnfonelemdc  13139  ennnfonelemjn  13142  ennnfonelemg  13143  ennnfonelemp1  13146  ennnfonelemom  13148  ennnfonelemhdmp1  13149  ennnfonelemss  13150  ennnfonelemkh  13152  ennnfonelemhf1o  13153  ennnfonelemex  13154  ennnfonelemhom  13155  ennnfonelemnn0  13162  ennnfonelemim  13164  ctinfomlemom  13167  ctiunctlemudc  13177  ctiunctlemf  13178  ctiunctlemfo  13179  ssnnctlemct  13186  nninfdclemp1  13190  nninfdclemlt  13191  imasmnd2  13654  mhmf1o  13672  mhmco  13692  gsumfzcl  13701  isgrpinv  13756  pwssub  13815  imasgrp2  13816  mhmid  13821  mhmmnd  13822  ghmgrp  13824  mulgval  13828  mulgfng  13830  mulgnnsubcl  13840  ghmid  13955  ghminv  13956  ghmmulg  13962  ghmnsgpreima  13975  ghmeqker  13977  ghmf1  13979  kerf1ghm  13980  ghmf1o  13981  gsumsplit0  14052  imasring  14197  rhmopp  14310  lspcl  14526  znidomb  14793  znrrg  14795  psrbaglesuppg  14808  psrbagfi  14810  psrbaglecl  14811  psrbagcon  14813  mplsubgfilemcl  14841  iscnp4  15070  cnptopco  15074  lmtopcnp  15102  upxp  15124  uptx  15126  txlm  15131  comet  15351  metcnp3  15363  metcnp  15364  metcnp2  15365  metcnpi3  15369  elcncf2  15426  cncfco  15443  ivthreinc  15497  limcimolemlt  15516  cnplimcim  15519  cnplimclemle  15520  cnplimclemr  15521  limccnpcntop  15527  dvlemap  15532  dvcnp2cntop  15551  dvaddxxbr  15553  dvmulxxbr  15554  dvcoapbr  15559  dvcjbr  15560  dvef  15579  plyaddlem1  15599  plymullem1  15600  plycoeid3  15609  plycolemc  15610  plycjlemc  15612  plycj  15613  plycn  15614  plyrecj  15615  dvply1  15617  dvply2g  15618  lgsval  15864  lgscllem  15867  lgsval2lem  15870  lgsval4a  15882  lgsneg  15884  lgsdir  15895  lgsdilem2  15896  lgsdi  15897  lgsne0  15898  lgseisenlem3  15932  lgseisenlem4  15933  p1evtxdeqfi  16294  wlkvtxm  16322  wlkvtxiedg  16327  wlkvtxiedgg  16328  upgriswlkdc  16342  trlsegvdeglem7  16448  trlsegvdegfi  16449  eupth2lem3lem1fi  16450  eupth2lem3lem2fi  16451  eupth2lem3lem3fi  16452  eupth2lem3lem6fi  16453  eupth2lem3lem4fi  16455  eupth2lem3lem7fi  16456  eupth2lemsfi  16460  3dom  16749  pwle2  16759  subctctexmid  16761  nnsf  16770  peano4nninf  16771  nninfalllem1  16773  nninfsellemdc  16775  nninfsellemeq  16779  nninfsellemqall  16780  nninfsellemeqinf  16781  nninfomnilem  16783  nnnninfex  16787  nninfnfiinf  16788  repiecelem  16796  repiecele0  16797  repiecege0  16798  isomninnlem  16801  trilpolemeq1  16811  trilpolemlt1  16812  iswomninnlem  16821  iswomni0  16823  ismkvnnlem  16824  nconstwlpolemgt0  16836  nconstwlpolem  16837  gfsumval  16848  gfsumcl  16856