Theorem ffvelcdmd 5776

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

Syntax hints:   → wi 4   ∈ wcel 2200  ⟶wf 5317  ‘cfv 5321

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4259  ax-pr 4294

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-id 4385  df-xp 4726  df-rel 4727  df-cnv 4728  df-co 4729  df-dm 4730  df-rn 4731  df-iota 5281  df-fun 5323  df-fn 5324  df-f 5325  df-fv 5329

This theorem is referenced by:  isotr  5949  caofinvl  6253  rdgon  6543  frecabcl  6556  phplem4dom  7036  fidceq  7044  dif1en  7054  fin0  7060  fin0or  7061  infm  7082  en2eqpr  7085  fidcenumlemrks  7136  fidcenumlemr  7138  supisoti  7193  ordiso2  7218  updjudhcoinlf  7263  updjudhcoinrg  7264  caseinl  7274  caseinr  7275  difinfsnlem  7282  difinfsn  7283  ctmlemr  7291  ctssdclemn0  7293  ctssdc  7296  enumctlemm  7297  enumct  7298  nnnninfeq2  7312  nninfisol  7316  enomnilem  7321  finomni  7323  ismkvnex  7338  enmkvlem  7344  enwomnilem  7352  nninfwlpoimlemg  7358  nninfwlpoimlemginf  7359  pr2cv1  7384  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  acnccim  7474  cauappcvgprlemm  7848  cauappcvgprlemdisj  7854  cauappcvgprlemloc  7855  cauappcvgprlemladdfu  7857  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  cauappcvgprlem1  7862  cauappcvgprlem2  7863  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemm  7871  caucvgprlemloc  7878  caucvgprlemladdfu  7880  caucvgprlemladdrl  7881  caucvgprlem1  7882  caucvgprlem2  7883  caucvgprprlemnkltj  7892  caucvgprprlemnkeqj  7893  caucvgprprlemnbj  7896  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemloc  7906  caucvgprprlemexbt  7909  caucvgprprlemexb  7910  caucvgprprlemaddq  7911  caucvgprprlem1  7912  caucvgprprlem2  7913  caucvgsrlemcau  7996  caucvgsrlemgt1  7998  caucvgsrlemoffcau  8001  caucvgsrlemoffres  8003  caucvgsr  8005  axcaucvglemval  8100  axcaucvglemcau  8101  axcaucvglemres  8102  fseq1p1m1  10307  4fvwrd4  10353  fvinim0ffz  10464  frecuzrdgg  10655  frecuzrdgsuctlem  10662  seq3val  10699  seqvalcd  10700  seq3p1  10704  seqp1cd  10709  ser3mono  10726  seq3split  10727  seq3caopr2  10732  iseqf1olemkle  10736  iseqf1olemklt  10737  iseqf1olemqcl  10738  iseqf1olemnab  10740  iseqf1olemmo  10744  iseqf1olemqk  10746  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  iseqf1olemfvp  10749  seq3f1olemqsumkj  10750  seq3f1olemqsumk  10751  seq3f1olemqsum  10752  seq3f1olemstep  10753  seq3f1oleml  10755  seq3f1o  10756  seqf1oglem2a  10757  seqf1oglem1  10758  seqf1oglem2  10759  seq3z  10767  seq3distr  10771  ser3ge0  10775  ser3le  10776  exp3vallem  10779  exp3val  10780  bcval5  11002  hashfz1  11022  resunimafz0  11071  leisorel  11077  zfz1isolemiso  11079  seq3coll  11082  ccatcl  11146  swrdclg  11203  caucvgrelemcau  11512  caucvgre  11513  cvg1nlemf  11515  cvg1nlemcau  11516  cvg1nlemres  11517  recvguniqlem  11526  resqrexlemdecn  11544  resqrexlemcalc3  11548  resqrexlemnmsq  11549  resqrexlemnm  11550  resqrexlemcvg  11551  resqrexlemoverl  11553  resqrexlemglsq  11554  resqrexlemga  11555  clim2ser  11869  clim2ser2  11870  climrecvg1n  11880  climcvg1nlem  11881  serf0  11884  sumeq2  11891  fsum3cvg  11910  summodclem2a  11913  fsum3  11919  fisumss  11924  fsumcl2lem  11930  fsumadd  11938  fsummulc2  11980  fsumrelem  12003  isumshft  12022  cvgratnnlemseq  12058  cvgratnnlemrate  12062  clim2prod  12071  clim2divap  12072  prodfrecap  12078  prodfdivap  12079  ntrivcvgap  12080  prodeq2  12089  fproddccvg  12104  prodmodclem3  12107  prodmodclem2a  12108  fprodseq  12115  fprodssdc  12122  fprodmul  12123  effsumlt  12224  nninfctlemfo  12582  nn0seqcvgd  12584  ialgrlem1st  12585  eulerthlemrprm  12772  eulerthlema  12773  eulerthlemh  12774  pcmpt2  12888  pcmptdvds  12889  1arithlem4  12910  1arith  12911  ennnfonelemdc  12991  ennnfonelemjn  12994  ennnfonelemg  12995  ennnfonelemp1  12998  ennnfonelemom  13000  ennnfonelemhdmp1  13001  ennnfonelemss  13002  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemex  13006  ennnfonelemhom  13007  ennnfonelemnn0  13014  ennnfonelemim  13016  ctinfomlemom  13019  ctiunctlemudc  13029  ctiunctlemf  13030  ctiunctlemfo  13031  ssnnctlemct  13038  nninfdclemp1  13042  nninfdclemlt  13043  imasmnd2  13506  mhmf1o  13524  mhmco  13544  gsumfzcl  13553  isgrpinv  13608  pwssub  13667  imasgrp2  13668  mhmid  13673  mhmmnd  13674  ghmgrp  13676  mulgval  13680  mulgfng  13682  mulgnnsubcl  13692  ghmid  13807  ghminv  13808  ghmmulg  13814  ghmnsgpreima  13827  ghmeqker  13829  ghmf1  13831  kerf1ghm  13832  ghmf1o  13833  imasring  14048  rhmopp  14161  lspcl  14376  znidomb  14643  znrrg  14645  psrbaglesuppg  14657  psrbagfi  14658  mplsubgfilemcl  14684  iscnp4  14913  cnptopco  14917  lmtopcnp  14945  upxp  14967  uptx  14969  txlm  14974  comet  15194  metcnp3  15206  metcnp  15207  metcnp2  15208  metcnpi3  15212  elcncf2  15269  cncfco  15286  ivthreinc  15340  limcimolemlt  15359  cnplimcim  15362  cnplimclemle  15363  cnplimclemr  15364  limccnpcntop  15370  dvlemap  15375  dvcnp2cntop  15394  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvcjbr  15403  dvef  15422  plyaddlem1  15442  plymullem1  15443  plycoeid3  15452  plycolemc  15453  plycjlemc  15455  plycj  15456  plycn  15457  plyrecj  15458  dvply1  15460  dvply2g  15461  lgsval  15704  lgscllem  15707  lgsval2lem  15710  lgsval4a  15722  lgsneg  15724  lgsdir  15735  lgsdilem2  15736  lgsdi  15737  lgsne0  15738  lgseisenlem3  15772  lgseisenlem4  15773  wlkvtxm  16112  wlkvtxiedg  16117  wlkvtxiedgg  16118  upgriswlkdc  16132  1dom1el  16463  3dom  16465  2omap  16472  pwle2  16477  subctctexmid  16479  nnsf  16485  peano4nninf  16486  nninfalllem1  16488  nninfsellemdc  16490  nninfsellemeq  16494  nninfsellemqall  16495  nninfsellemeqinf  16496  nninfomnilem  16498  nnnninfex  16502  nninfnfiinf  16503  isomninnlem  16512  trilpolemeq1  16522  trilpolemlt1  16523  iswomninnlem  16531  iswomni0  16533  ismkvnnlem  16534  nconstwlpolemgt0  16546  nconstwlpolem  16547