Theorem ffvelcdmd 5818

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

Syntax hints:   → wi 4   ∈ wcel 2205  ⟶wf 5353  ‘cfv 5357

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 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-fv 5365

This theorem is referenced by:  isotr  5995  caofinvl  6301  fvdifsuppst  6457  rdgon  6630  frecabcl  6643  1dom1el  7073  phplem4dom  7129  fidceq  7137  dif1en  7149  fin0  7155  fin0or  7156  infm  7177  en2eqpr  7180  fidcenumlemrks  7236  fidcenumlemr  7238  2omap  7282  supisoti  7314  ordiso2  7339  updjudhcoinlf  7384  updjudhcoinrg  7385  caseinl  7395  caseinr  7396  difinfsnlem  7403  difinfsn  7404  ctmlemr  7412  ctssdclemn0  7414  ctssdc  7417  enumctlemm  7418  enumct  7419  nnnninfeq2  7433  nninfisol  7437  enomnilem  7442  finomni  7444  ismkvnex  7459  enmkvlem  7465  enwomnilem  7473  nninfwlpoimlemg  7479  nninfwlpoimlemginf  7480  pr2cv1  7505  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  acnccim  7602  cauappcvgprlemm  7976  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlem2  7991  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgprlem2  8011  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnbj  8024  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemexb  8038  caucvgprprlemaddq  8039  caucvgprprlem1  8040  caucvgprprlem2  8041  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  caucvgsr  8133  axcaucvglemval  8228  axcaucvglemcau  8229  axcaucvglemres  8230  fseq1p1m1  10453  4fvwrd4  10499  fvinim0ffz  10612  frecuzrdgg  10805  frecuzrdgsuctlem  10812  seq3val  10849  seqvalcd  10850  seq3p1  10854  seqp1cd  10859  ser3mono  10876  seq3split  10877  seq3caopr2  10882  iseqf1olemkle  10886  iseqf1olemklt  10887  iseqf1olemqcl  10888  iseqf1olemnab  10890  iseqf1olemmo  10894  iseqf1olemqk  10896  iseqf1olemjpcl  10897  iseqf1olemqpcl  10898  iseqf1olemfvp  10899  seq3f1olemqsumkj  10900  seq3f1olemqsumk  10901  seq3f1olemqsum  10902  seq3f1olemstep  10903  seq3f1oleml  10905  seq3f1o  10906  seqf1oglem2a  10907  seqf1oglem1  10908  seqf1oglem2  10909  seq3z  10917  seq3distr  10921  ser3ge0  10925  ser3le  10926  exp3vallem  10929  exp3val  10930  bcval5  11153  hashfz1  11174  resunimafz0  11226  leisorel  11237  zfz1isolemiso  11239  seq3coll  11242  ccatcl  11309  swrdclg  11370  caucvgrelemcau  11693  caucvgre  11694  cvg1nlemf  11696  cvg1nlemcau  11697  cvg1nlemres  11698  recvguniqlem  11707  resqrexlemdecn  11725  resqrexlemcalc3  11729  resqrexlemnmsq  11730  resqrexlemnm  11731  resqrexlemcvg  11732  resqrexlemoverl  11734  resqrexlemglsq  11735  resqrexlemga  11736  clim2ser  12050  clim2ser2  12051  climrecvg1n  12061  climcvg1nlem  12062  serf0  12065  sumeq2  12072  fsum3cvg  12092  summodclem2a  12095  fsum3  12101  fisumss  12106  fsumcl2lem  12112  fsumadd  12120  fsummulc2  12162  fsumrelem  12185  isumshft  12204  cvgratnnlemseq  12240  cvgratnnlemrate  12244  clim2prod  12253  clim2divap  12254  prodfrecap  12260  prodfdivap  12261  ntrivcvgap  12262  prodeq2  12271  fproddccvg  12286  prodmodclem3  12289  prodmodclem2a  12290  fprodseq  12297  fprodssdc  12304  fprodmul  12305  effsumlt  12406  nninfctlemfo  12764  nn0seqcvgd  12766  ialgrlem1st  12767  eulerthlemrprm  12954  eulerthlema  12955  eulerthlemh  12956  pcmpt2  13070  pcmptdvds  13071  1arithlem4  13092  1arith  13093  ennnfonelemdc  13237  ennnfonelemjn  13240  ennnfonelemg  13241  ennnfonelemp1  13244  ennnfonelemom  13246  ennnfonelemhdmp1  13247  ennnfonelemss  13248  ennnfonelemkh  13250  ennnfonelemhf1o  13251  ennnfonelemex  13252  ennnfonelemhom  13253  ennnfonelemnn0  13260  ennnfonelemim  13262  ctinfomlemom  13265  ctiunctlemudc  13275  ctiunctlemf  13276  ctiunctlemfo  13277  ssnnctlemct  13284  nninfdclemp1  13288  nninfdclemlt  13289  imasmnd2  13710  mhmf1o  13728  mhmco  13748  gsumfzcl  13757  isgrpinv  13812  imasgrp2  13866  mhmid  13871  mhmmnd  13872  ghmgrp  13874  mulgval  13878  mulgfng  13880  mulgnnsubcl  13890  ghmid  14005  ghminv  14006  ghmmulg  14012  ghmnsgpreima  14025  ghmeqker  14027  ghmf1  14029  kerf1ghm  14030  ghmf1o  14031  gsumsplit0  14102  gfsumval  14105  gfsumcl  14113  pwssub  14161  imasring  14310  rhmopp  14424  lspcl  14668  znidomb  14935  znrrg  14937  psrbaglesuppg  14950  psrbagfi  14952  psrbaglecl  14953  psrbagcon  14955  mplsubgfilemcl  14983  iscnp4  15212  cnptopco  15216  lmtopcnp  15244  upxp  15266  uptx  15268  txlm  15273  comet  15493  metcnp3  15505  metcnp  15506  metcnp2  15507  metcnpi3  15511  elcncf2  15568  cncfco  15585  ivthreinc  15639  limcimolemlt  15658  cnplimcim  15661  cnplimclemle  15662  cnplimclemr  15663  limccnpcntop  15669  dvlemap  15674  dvcnp2cntop  15693  dvaddxxbr  15695  dvmulxxbr  15696  dvcoapbr  15701  dvcjbr  15702  dvef  15721  plyaddlem1  15741  plymullem1  15742  plycoeid3  15751  plycolemc  15752  plycjlemc  15754  plycj  15755  plycn  15756  plyrecj  15757  dvply1  15759  dvply2g  15760  lgsval  16006  lgscllem  16009  lgsval2lem  16012  lgsval4a  16024  lgsneg  16026  lgsdir  16037  lgsdilem2  16038  lgsdi  16039  lgsne0  16040  lgseisenlem3  16074  lgseisenlem4  16075  p1evtxdeqfi  16436  wlkvtxm  16464  wlkvtxiedg  16469  wlkvtxiedgg  16470  upgriswlkdc  16484  trlsegvdeglem7  16590  trlsegvdegfi  16591  eupth2lem3lem1fi  16592  eupth2lem3lem2fi  16593  eupth2lem3lem3fi  16594  eupth2lem3lem6fi  16595  eupth2lem3lem4fi  16597  eupth2lem3lem7fi  16598  eupth2lemsfi  16602  3dom  16901  pwle2  16911  subctctexmid  16913  nnsf  16922  peano4nninf  16923  nninfalllem1  16925  nninfsellemdc  16927  nninfsellemeq  16931  nninfsellemqall  16932  nninfsellemeqinf  16933  nninfomnilem  16935  nnnninfex  16939  nninfnfiinf  16940  repiecelem  16948  repiecele0  16949  repiecege0  16950  isomninnlem  16953  trilpolemeq1  16963  trilpolemlt1  16964  iswomninnlem  16973  iswomni0  16975  ismkvnnlem  16976  nconstwlpolemgt0  16989  nconstwlpolem  16990