Theorem ffvelcdmd 5820

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

Syntax hints:   → wi 4   ∈ wcel 2205  ⟶wf 5355  ‘cfv 5359

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 4234  ax-pow 4293  ax-pr 4328

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 3677  df-sn 3701  df-pr 3702  df-op 3704  df-uni 3921  df-br 4116  df-opab 4178  df-id 4420  df-xp 4762  df-rel 4763  df-cnv 4764  df-co 4765  df-dm 4766  df-rn 4767  df-iota 5319  df-fun 5361  df-fn 5362  df-f 5363  df-fv 5367

This theorem is referenced by:  isotr  5997  caofinvl  6303  fvdifsuppst  6459  rdgon  6632  frecabcl  6645  1dom1el  7075  phplem4dom  7131  fidceq  7139  dif1en  7151  fin0  7157  fin0or  7158  infm  7179  en2eqpr  7182  fidcenumlemrks  7238  fidcenumlemr  7240  2omap  7284  supisoti  7316  ordiso2  7341  updjudhcoinlf  7386  updjudhcoinrg  7387  caseinl  7397  caseinr  7398  difinfsnlem  7405  difinfsn  7406  ctmlemr  7414  ctssdclemn0  7416  ctssdc  7419  enumctlemm  7420  enumct  7421  nnnninfeq2  7435  nninfisol  7439  enomnilem  7444  finomni  7446  ismkvnex  7461  enmkvlem  7467  enwomnilem  7475  nninfwlpoimlemg  7481  nninfwlpoimlemginf  7482  pr2cv1  7507  exmidfodomrlemr  7520  exmidfodomrlemrALT  7521  acnccim  7604  cauappcvgprlemm  7978  cauappcvgprlemdisj  7984  cauappcvgprlemloc  7985  cauappcvgprlemladdfu  7987  cauappcvgprlemladdru  7989  cauappcvgprlemladdrl  7990  cauappcvgprlem1  7992  cauappcvgprlem2  7993  caucvgprlemnkj  7999  caucvgprlemnbj  8000  caucvgprlemm  8001  caucvgprlemloc  8008  caucvgprlemladdfu  8010  caucvgprlemladdrl  8011  caucvgprlem1  8012  caucvgprlem2  8013  caucvgprprlemnkltj  8022  caucvgprprlemnkeqj  8023  caucvgprprlemnbj  8026  caucvgprprlemmu  8028  caucvgprprlemopl  8030  caucvgprprlemloc  8036  caucvgprprlemexbt  8039  caucvgprprlemexb  8040  caucvgprprlemaddq  8041  caucvgprprlem1  8042  caucvgprprlem2  8043  caucvgsrlemcau  8126  caucvgsrlemgt1  8128  caucvgsrlemoffcau  8131  caucvgsrlemoffres  8133  caucvgsr  8135  axcaucvglemval  8230  axcaucvglemcau  8231  axcaucvglemres  8232  fseq1p1m1  10455  4fvwrd4  10501  fvinim0ffz  10614  frecuzrdgg  10807  frecuzrdgsuctlem  10814  seq3val  10851  seqvalcd  10852  seq3p1  10856  seqp1cd  10861  ser3mono  10878  seq3split  10879  seq3caopr2  10884  iseqf1olemkle  10888  iseqf1olemklt  10889  iseqf1olemqcl  10890  iseqf1olemnab  10892  iseqf1olemmo  10896  iseqf1olemqk  10898  iseqf1olemjpcl  10899  iseqf1olemqpcl  10900  iseqf1olemfvp  10901  seq3f1olemqsumkj  10902  seq3f1olemqsumk  10903  seq3f1olemqsum  10904  seq3f1olemstep  10905  seq3f1oleml  10907  seq3f1o  10908  seqf1oglem2a  10909  seqf1oglem1  10910  seqf1oglem2  10911  seq3z  10919  seq3distr  10923  ser3ge0  10927  ser3le  10928  exp3vallem  10931  exp3val  10932  bcval5  11155  hashfz1  11176  resunimafz0  11228  leisorel  11239  zfz1isolemiso  11241  seq3coll  11244  ccatcl  11311  swrdclg  11372  caucvgrelemcau  11696  caucvgre  11697  cvg1nlemf  11699  cvg1nlemcau  11700  cvg1nlemres  11701  recvguniqlem  11710  resqrexlemdecn  11728  resqrexlemcalc3  11732  resqrexlemnmsq  11733  resqrexlemnm  11734  resqrexlemcvg  11735  resqrexlemoverl  11737  resqrexlemglsq  11738  resqrexlemga  11739  clim2ser  12053  clim2ser2  12054  climrecvg1n  12064  climcvg1nlem  12065  serf0  12068  sumeq2  12075  fsum3cvg  12095  summodclem2a  12098  fsum3  12104  fisumss  12109  fsumcl2lem  12115  fsumadd  12123  fsummulc2  12165  fsumrelem  12188  isumshft  12207  cvgratnnlemseq  12243  cvgratnnlemrate  12247  clim2prod  12256  clim2divap  12257  prodfrecap  12263  prodfdivap  12264  ntrivcvgap  12265  prodeq2  12274  fproddccvg  12289  prodmodclem3  12292  prodmodclem2a  12293  fprodseq  12300  fprodssdc  12307  fprodmul  12308  effsumlt  12409  nninfctlemfo  12767  nn0seqcvgd  12769  ialgrlem1st  12770  eulerthlemrprm  12957  eulerthlema  12958  eulerthlemh  12959  pcmpt2  13073  pcmptdvds  13074  1arithlem4  13095  1arith  13096  ennnfonelemdc  13240  ennnfonelemjn  13243  ennnfonelemg  13244  ennnfonelemp1  13247  ennnfonelemom  13249  ennnfonelemhdmp1  13250  ennnfonelemss  13251  ennnfonelemkh  13253  ennnfonelemhf1o  13254  ennnfonelemex  13255  ennnfonelemhom  13256  ennnfonelemnn0  13263  ennnfonelemim  13265  ctinfomlemom  13268  ctiunctlemudc  13278  ctiunctlemf  13279  ctiunctlemfo  13280  ssnnctlemct  13287  nninfdclemp1  13291  nninfdclemlt  13292  imasmnd2  13708  mhmf1o  13726  mhmco  13746  gzsumcl  13753  isgrpinv  13808  imasgrp2  13862  mhmid  13867  mhmmnd  13868  ghmgrp  13870  mulgval  13874  mulgfng  13876  mulgnnsubcl  13886  ghmid  14001  ghminv  14002  ghmmulg  14008  ghmnsgpreima  14021  ghmeqker  14023  ghmf1  14025  kerf1ghm  14026  ghmf1o  14027  gzsumsplit0  14097  gsumvalfi  14101  gsumclfi  14108  gsumsubmclfi  14112  pwssub  14165  imasring  14314  rhmopp  14428  lspcl  14672  znidomb  14937  znrrg  14939  psrbaglesuppg  14952  psrbagfi  14954  psrbaglecl  14955  psrbagcon  14957  mplsubgfilemcl  14985  iscnp4  15214  cnptopco  15218  lmtopcnp  15246  upxp  15268  uptx  15270  txlm  15275  comet  15495  metcnp3  15507  metcnp  15508  metcnp2  15509  metcnpi3  15513  elcncf2  15570  cncfco  15587  ivthreinc  15641  limcimolemlt  15660  cnplimcim  15663  cnplimclemle  15664  cnplimclemr  15665  limccnpcntop  15671  dvlemap  15676  dvcnp2cntop  15695  dvaddxxbr  15697  dvmulxxbr  15698  dvcoapbr  15703  dvcjbr  15704  dvef  15723  plyaddlem1  15743  plymullem1  15744  plycoeid3  15753  plycolemc  15754  plycjlemc  15756  plycj  15757  plycn  15758  plyrecj  15759  dvply1  15761  dvply2g  15762  lgsval  16008  lgscllem  16011  lgsval2lem  16014  lgsval4a  16026  lgsneg  16028  lgsdir  16039  lgsdilem2  16040  lgsdi  16041  lgsne0  16042  lgseisenlem3  16076  lgseisenlem4  16077  p1evtxdeqfi  16438  wlkvtxm  16466  wlkvtxiedg  16471  wlkvtxiedgg  16472  upgriswlkdc  16486  trlsegvdeglem7  16592  trlsegvdegfi  16593  eupth2lem3lem1fi  16594  eupth2lem3lem2fi  16595  eupth2lem3lem3fi  16596  eupth2lem3lem6fi  16597  eupth2lem3lem4fi  16599  eupth2lem3lem7fi  16600  eupth2lemsfi  16604  3dom  16903  pwle2  16913  subctctexmid  16915  nnsf  16924  peano4nninf  16925  nninfalllem1  16927  nninfsellemdc  16929  nninfsellemeq  16933  nninfsellemqall  16934  nninfsellemeqinf  16935  nninfomnilem  16937  nnnninfex  16941  nninfnfiinf  16942  repiecelem  16950  repiecele0  16951  repiecege0  16952  isomninnlem  16955  trilpolemeq1  16965  trilpolemlt1  16966  iswomninnlem  16975  iswomni0  16977  ismkvnnlem  16978  nconstwlpolemgt0  16990  nconstwlpolem  16991