Theorem ffvelcdmd 5786

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

Syntax hints:   → wi 4   ∈ wcel 2201  ⟶wf 5324  ‘cfv 5328

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-sbc 3031  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-opab 4152  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-iota 5288  df-fun 5330  df-fn 5331  df-f 5332  df-fv 5336

This theorem is referenced by:  isotr  5962  caofinvl  6266  rdgon  6557  frecabcl  6570  1dom1el  6998  phplem4dom  7053  fidceq  7061  dif1en  7073  fin0  7079  fin0or  7080  infm  7101  en2eqpr  7104  fidcenumlemrks  7157  fidcenumlemr  7159  supisoti  7214  ordiso2  7239  updjudhcoinlf  7284  updjudhcoinrg  7285  caseinl  7295  caseinr  7296  difinfsnlem  7303  difinfsn  7304  ctmlemr  7312  ctssdclemn0  7314  ctssdc  7317  enumctlemm  7318  enumct  7319  nnnninfeq2  7333  nninfisol  7337  enomnilem  7342  finomni  7344  ismkvnex  7359  enmkvlem  7365  enwomnilem  7373  nninfwlpoimlemg  7379  nninfwlpoimlemginf  7380  pr2cv1  7405  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  acnccim  7496  cauappcvgprlemm  7870  cauappcvgprlemdisj  7876  cauappcvgprlemloc  7877  cauappcvgprlemladdfu  7879  cauappcvgprlemladdru  7881  cauappcvgprlemladdrl  7882  cauappcvgprlem1  7884  cauappcvgprlem2  7885  caucvgprlemnkj  7891  caucvgprlemnbj  7892  caucvgprlemm  7893  caucvgprlemloc  7900  caucvgprlemladdfu  7902  caucvgprlemladdrl  7903  caucvgprlem1  7904  caucvgprlem2  7905  caucvgprprlemnkltj  7914  caucvgprprlemnkeqj  7915  caucvgprprlemnbj  7918  caucvgprprlemmu  7920  caucvgprprlemopl  7922  caucvgprprlemloc  7928  caucvgprprlemexbt  7931  caucvgprprlemexb  7932  caucvgprprlemaddq  7933  caucvgprprlem1  7934  caucvgprprlem2  7935  caucvgsrlemcau  8018  caucvgsrlemgt1  8020  caucvgsrlemoffcau  8023  caucvgsrlemoffres  8025  caucvgsr  8027  axcaucvglemval  8122  axcaucvglemcau  8123  axcaucvglemres  8124  fseq1p1m1  10334  4fvwrd4  10380  fvinim0ffz  10493  frecuzrdgg  10684  frecuzrdgsuctlem  10691  seq3val  10728  seqvalcd  10729  seq3p1  10733  seqp1cd  10738  ser3mono  10755  seq3split  10756  seq3caopr2  10761  iseqf1olemkle  10765  iseqf1olemklt  10766  iseqf1olemqcl  10767  iseqf1olemnab  10769  iseqf1olemmo  10773  iseqf1olemqk  10775  iseqf1olemjpcl  10776  iseqf1olemqpcl  10777  iseqf1olemfvp  10778  seq3f1olemqsumkj  10779  seq3f1olemqsumk  10780  seq3f1olemqsum  10781  seq3f1olemstep  10782  seq3f1oleml  10784  seq3f1o  10785  seqf1oglem2a  10786  seqf1oglem1  10787  seqf1oglem2  10788  seq3z  10796  seq3distr  10800  ser3ge0  10804  ser3le  10805  exp3vallem  10808  exp3val  10809  bcval5  11031  hashfz1  11051  resunimafz0  11101  leisorel  11107  zfz1isolemiso  11109  seq3coll  11112  ccatcl  11179  swrdclg  11240  caucvgrelemcau  11563  caucvgre  11564  cvg1nlemf  11566  cvg1nlemcau  11567  cvg1nlemres  11568  recvguniqlem  11577  resqrexlemdecn  11595  resqrexlemcalc3  11599  resqrexlemnmsq  11600  resqrexlemnm  11601  resqrexlemcvg  11602  resqrexlemoverl  11604  resqrexlemglsq  11605  resqrexlemga  11606  clim2ser  11920  clim2ser2  11921  climrecvg1n  11931  climcvg1nlem  11932  serf0  11935  sumeq2  11942  fsum3cvg  11962  summodclem2a  11965  fsum3  11971  fisumss  11976  fsumcl2lem  11982  fsumadd  11990  fsummulc2  12032  fsumrelem  12055  isumshft  12074  cvgratnnlemseq  12110  cvgratnnlemrate  12114  clim2prod  12123  clim2divap  12124  prodfrecap  12130  prodfdivap  12131  ntrivcvgap  12132  prodeq2  12141  fproddccvg  12156  prodmodclem3  12159  prodmodclem2a  12160  fprodseq  12167  fprodssdc  12174  fprodmul  12175  effsumlt  12276  nninfctlemfo  12634  nn0seqcvgd  12636  ialgrlem1st  12637  eulerthlemrprm  12824  eulerthlema  12825  eulerthlemh  12826  pcmpt2  12940  pcmptdvds  12941  1arithlem4  12962  1arith  12963  ennnfonelemdc  13043  ennnfonelemjn  13046  ennnfonelemg  13047  ennnfonelemp1  13050  ennnfonelemom  13052  ennnfonelemhdmp1  13053  ennnfonelemss  13054  ennnfonelemkh  13056  ennnfonelemhf1o  13057  ennnfonelemex  13058  ennnfonelemhom  13059  ennnfonelemnn0  13066  ennnfonelemim  13068  ctinfomlemom  13071  ctiunctlemudc  13081  ctiunctlemf  13082  ctiunctlemfo  13083  ssnnctlemct  13090  nninfdclemp1  13094  nninfdclemlt  13095  imasmnd2  13558  mhmf1o  13576  mhmco  13596  gsumfzcl  13605  isgrpinv  13660  pwssub  13719  imasgrp2  13720  mhmid  13725  mhmmnd  13726  ghmgrp  13728  mulgval  13732  mulgfng  13734  mulgnnsubcl  13744  ghmid  13859  ghminv  13860  ghmmulg  13866  ghmnsgpreima  13879  ghmeqker  13881  ghmf1  13883  kerf1ghm  13884  ghmf1o  13885  gsumsplit0  13956  imasring  14101  rhmopp  14214  lspcl  14429  znidomb  14696  znrrg  14698  psrbaglesuppg  14710  psrbagfi  14712  psrbaglecl  14713  psrbagcon  14714  mplsubgfilemcl  14742  iscnp4  14971  cnptopco  14975  lmtopcnp  15003  upxp  15025  uptx  15027  txlm  15032  comet  15252  metcnp3  15264  metcnp  15265  metcnp2  15266  metcnpi3  15270  elcncf2  15327  cncfco  15344  ivthreinc  15398  limcimolemlt  15417  cnplimcim  15420  cnplimclemle  15421  cnplimclemr  15422  limccnpcntop  15428  dvlemap  15433  dvcnp2cntop  15452  dvaddxxbr  15454  dvmulxxbr  15455  dvcoapbr  15460  dvcjbr  15461  dvef  15480  plyaddlem1  15500  plymullem1  15501  plycoeid3  15510  plycolemc  15511  plycjlemc  15513  plycj  15514  plycn  15515  plyrecj  15516  dvply1  15518  dvply2g  15519  lgsval  15762  lgscllem  15765  lgsval2lem  15768  lgsval4a  15780  lgsneg  15782  lgsdir  15793  lgsdilem2  15794  lgsdi  15795  lgsne0  15796  lgseisenlem3  15830  lgseisenlem4  15831  p1evtxdeqfi  16192  wlkvtxm  16220  wlkvtxiedg  16225  wlkvtxiedgg  16226  upgriswlkdc  16240  trlsegvdeglem7  16346  trlsegvdegfi  16347  eupth2lem3lem1fi  16348  eupth2lem3lem2fi  16349  eupth2lem3lem3fi  16350  eupth2lem3lem6fi  16351  eupth2lem3lem4fi  16353  eupth2lem3lem7fi  16354  eupth2lemsfi  16358  3dom  16647  2omap  16654  pwle2  16659  subctctexmid  16661  nnsf  16670  peano4nninf  16671  nninfalllem1  16673  nninfsellemdc  16675  nninfsellemeq  16679  nninfsellemqall  16680  nninfsellemeqinf  16681  nninfomnilem  16683  nnnninfex  16687  nninfnfiinf  16688  repiecelem  16696  repiecele0  16697  repiecege0  16698  isomninnlem  16701  trilpolemeq1  16711  trilpolemlt1  16712  iswomninnlem  16721  iswomni0  16723  ismkvnnlem  16724  nconstwlpolemgt0  16736  nconstwlpolem  16737  gfsumval  16748  gfsumcl  16755