Theorem ffvelcdmd 5744

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

Syntax hints:   → wi 4   ∈ wcel 2180  ⟶wf 5290  ‘cfv 5294

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-sbc 3009  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-opab 4125  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-fv 5302

This theorem is referenced by:  isotr  5913  caofinvl  6214  rdgon  6502  frecabcl  6515  phplem4dom  6991  fidceq  6999  dif1en  7009  fin0  7015  fin0or  7016  infm  7034  en2eqpr  7037  fidcenumlemrks  7088  fidcenumlemr  7090  supisoti  7145  ordiso2  7170  updjudhcoinlf  7215  updjudhcoinrg  7216  caseinl  7226  caseinr  7227  difinfsnlem  7234  difinfsn  7235  ctmlemr  7243  ctssdclemn0  7245  ctssdc  7248  enumctlemm  7249  enumct  7250  nnnninfeq2  7264  nninfisol  7268  enomnilem  7273  finomni  7275  ismkvnex  7290  enmkvlem  7296  enwomnilem  7304  nninfwlpoimlemg  7310  nninfwlpoimlemginf  7311  pr2cv1  7336  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  acnccim  7426  cauappcvgprlemm  7800  cauappcvgprlemdisj  7806  cauappcvgprlemloc  7807  cauappcvgprlemladdfu  7809  cauappcvgprlemladdru  7811  cauappcvgprlemladdrl  7812  cauappcvgprlem1  7814  cauappcvgprlem2  7815  caucvgprlemnkj  7821  caucvgprlemnbj  7822  caucvgprlemm  7823  caucvgprlemloc  7830  caucvgprlemladdfu  7832  caucvgprlemladdrl  7833  caucvgprlem1  7834  caucvgprlem2  7835  caucvgprprlemnkltj  7844  caucvgprprlemnkeqj  7845  caucvgprprlemnbj  7848  caucvgprprlemmu  7850  caucvgprprlemopl  7852  caucvgprprlemloc  7858  caucvgprprlemexbt  7861  caucvgprprlemexb  7862  caucvgprprlemaddq  7863  caucvgprprlem1  7864  caucvgprprlem2  7865  caucvgsrlemcau  7948  caucvgsrlemgt1  7950  caucvgsrlemoffcau  7953  caucvgsrlemoffres  7955  caucvgsr  7957  axcaucvglemval  8052  axcaucvglemcau  8053  axcaucvglemres  8054  fseq1p1m1  10258  4fvwrd4  10304  fvinim0ffz  10414  frecuzrdgg  10605  frecuzrdgsuctlem  10612  seq3val  10649  seqvalcd  10650  seq3p1  10654  seqp1cd  10659  ser3mono  10676  seq3split  10677  seq3caopr2  10682  iseqf1olemkle  10686  iseqf1olemklt  10687  iseqf1olemqcl  10688  iseqf1olemnab  10690  iseqf1olemmo  10694  iseqf1olemqk  10696  iseqf1olemjpcl  10697  iseqf1olemqpcl  10698  iseqf1olemfvp  10699  seq3f1olemqsumkj  10700  seq3f1olemqsumk  10701  seq3f1olemqsum  10702  seq3f1olemstep  10703  seq3f1oleml  10705  seq3f1o  10706  seqf1oglem2a  10707  seqf1oglem1  10708  seqf1oglem2  10709  seq3z  10717  seq3distr  10721  ser3ge0  10725  ser3le  10726  exp3vallem  10729  exp3val  10730  bcval5  10952  hashfz1  10972  resunimafz0  11020  leisorel  11026  zfz1isolemiso  11028  seq3coll  11031  ccatcl  11094  swrdclg  11148  caucvgrelemcau  11457  caucvgre  11458  cvg1nlemf  11460  cvg1nlemcau  11461  cvg1nlemres  11462  recvguniqlem  11471  resqrexlemdecn  11489  resqrexlemcalc3  11493  resqrexlemnmsq  11494  resqrexlemnm  11495  resqrexlemcvg  11496  resqrexlemoverl  11498  resqrexlemglsq  11499  resqrexlemga  11500  clim2ser  11814  clim2ser2  11815  climrecvg1n  11825  climcvg1nlem  11826  serf0  11829  sumeq2  11836  fsum3cvg  11855  summodclem2a  11858  fsum3  11864  fisumss  11869  fsumcl2lem  11875  fsumadd  11883  fsummulc2  11925  fsumrelem  11948  isumshft  11967  cvgratnnlemseq  12003  cvgratnnlemrate  12007  clim2prod  12016  clim2divap  12017  prodfrecap  12023  prodfdivap  12024  ntrivcvgap  12025  prodeq2  12034  fproddccvg  12049  prodmodclem3  12052  prodmodclem2a  12053  fprodseq  12060  fprodssdc  12067  fprodmul  12068  effsumlt  12169  nninfctlemfo  12527  nn0seqcvgd  12529  ialgrlem1st  12530  eulerthlemrprm  12717  eulerthlema  12718  eulerthlemh  12719  pcmpt2  12833  pcmptdvds  12834  1arithlem4  12855  1arith  12856  ennnfonelemdc  12936  ennnfonelemjn  12939  ennnfonelemg  12940  ennnfonelemp1  12943  ennnfonelemom  12945  ennnfonelemhdmp1  12946  ennnfonelemss  12947  ennnfonelemkh  12949  ennnfonelemhf1o  12950  ennnfonelemex  12951  ennnfonelemhom  12952  ennnfonelemnn0  12959  ennnfonelemim  12961  ctinfomlemom  12964  ctiunctlemudc  12974  ctiunctlemf  12975  ctiunctlemfo  12976  ssnnctlemct  12983  nninfdclemp1  12987  nninfdclemlt  12988  imasmnd2  13451  mhmf1o  13469  mhmco  13489  gsumfzcl  13498  isgrpinv  13553  pwssub  13612  imasgrp2  13613  mhmid  13618  mhmmnd  13619  ghmgrp  13621  mulgval  13625  mulgfng  13627  mulgnnsubcl  13637  ghmid  13752  ghminv  13753  ghmmulg  13759  ghmnsgpreima  13772  ghmeqker  13774  ghmf1  13776  kerf1ghm  13777  ghmf1o  13778  imasring  13993  rhmopp  14105  lspcl  14320  znidomb  14587  znrrg  14589  psrbaglesuppg  14601  psrbagfi  14602  mplsubgfilemcl  14628  iscnp4  14857  cnptopco  14861  lmtopcnp  14889  upxp  14911  uptx  14913  txlm  14918  comet  15138  metcnp3  15150  metcnp  15151  metcnp2  15152  metcnpi3  15156  elcncf2  15213  cncfco  15230  ivthreinc  15284  limcimolemlt  15303  cnplimcim  15306  cnplimclemle  15307  cnplimclemr  15308  limccnpcntop  15314  dvlemap  15319  dvcnp2cntop  15338  dvaddxxbr  15340  dvmulxxbr  15341  dvcoapbr  15346  dvcjbr  15347  dvef  15366  plyaddlem1  15386  plymullem1  15387  plycoeid3  15396  plycolemc  15397  plycjlemc  15399  plycj  15400  plycn  15401  plyrecj  15402  dvply1  15404  dvply2g  15405  lgsval  15648  lgscllem  15651  lgsval2lem  15654  lgsval4a  15666  lgsneg  15668  lgsdir  15679  lgsdilem2  15680  lgsdi  15681  lgsne0  15682  lgseisenlem3  15716  lgseisenlem4  15717  1dom1el  16264  2omap  16270  pwle2  16275  subctctexmid  16277  nnsf  16282  peano4nninf  16283  nninfalllem1  16285  nninfsellemdc  16287  nninfsellemeq  16291  nninfsellemqall  16292  nninfsellemeqinf  16293  nninfomnilem  16295  nnnninfex  16299  nninfnfiinf  16300  isomninnlem  16309  trilpolemeq1  16319  trilpolemlt1  16320  iswomninnlem  16328  iswomni0  16330  ismkvnnlem  16331  nconstwlpolemgt0  16343  nconstwlpolem  16344