Theorem ffvelcdmd 5773

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

Syntax hints:   → wi 4   ∈ wcel 2200  ⟶wf 5314  ‘cfv 5318

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 4258  ax-pr 4293

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 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-fv 5326

This theorem is referenced by:  isotr  5946  caofinvl  6250  rdgon  6538  frecabcl  6551  phplem4dom  7031  fidceq  7039  dif1en  7049  fin0  7055  fin0or  7056  infm  7074  en2eqpr  7077  fidcenumlemrks  7128  fidcenumlemr  7130  supisoti  7185  ordiso2  7210  updjudhcoinlf  7255  updjudhcoinrg  7256  caseinl  7266  caseinr  7267  difinfsnlem  7274  difinfsn  7275  ctmlemr  7283  ctssdclemn0  7285  ctssdc  7288  enumctlemm  7289  enumct  7290  nnnninfeq2  7304  nninfisol  7308  enomnilem  7313  finomni  7315  ismkvnex  7330  enmkvlem  7336  enwomnilem  7344  nninfwlpoimlemg  7350  nninfwlpoimlemginf  7351  pr2cv1  7376  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  acnccim  7466  cauappcvgprlemm  7840  cauappcvgprlemdisj  7846  cauappcvgprlemloc  7847  cauappcvgprlemladdfu  7849  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  cauappcvgprlem1  7854  cauappcvgprlem2  7855  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemm  7863  caucvgprlemloc  7870  caucvgprlemladdfu  7872  caucvgprlemladdrl  7873  caucvgprlem1  7874  caucvgprlem2  7875  caucvgprprlemnkltj  7884  caucvgprprlemnkeqj  7885  caucvgprprlemnbj  7888  caucvgprprlemmu  7890  caucvgprprlemopl  7892  caucvgprprlemloc  7898  caucvgprprlemexbt  7901  caucvgprprlemexb  7902  caucvgprprlemaddq  7903  caucvgprprlem1  7904  caucvgprprlem2  7905  caucvgsrlemcau  7988  caucvgsrlemgt1  7990  caucvgsrlemoffcau  7993  caucvgsrlemoffres  7995  caucvgsr  7997  axcaucvglemval  8092  axcaucvglemcau  8093  axcaucvglemres  8094  fseq1p1m1  10298  4fvwrd4  10344  fvinim0ffz  10455  frecuzrdgg  10646  frecuzrdgsuctlem  10653  seq3val  10690  seqvalcd  10691  seq3p1  10695  seqp1cd  10700  ser3mono  10717  seq3split  10718  seq3caopr2  10723  iseqf1olemkle  10727  iseqf1olemklt  10728  iseqf1olemqcl  10729  iseqf1olemnab  10731  iseqf1olemmo  10735  iseqf1olemqk  10737  iseqf1olemjpcl  10738  iseqf1olemqpcl  10739  iseqf1olemfvp  10740  seq3f1olemqsumkj  10741  seq3f1olemqsumk  10742  seq3f1olemqsum  10743  seq3f1olemstep  10744  seq3f1oleml  10746  seq3f1o  10747  seqf1oglem2a  10748  seqf1oglem1  10749  seqf1oglem2  10750  seq3z  10758  seq3distr  10762  ser3ge0  10766  ser3le  10767  exp3vallem  10770  exp3val  10771  bcval5  10993  hashfz1  11013  resunimafz0  11061  leisorel  11067  zfz1isolemiso  11069  seq3coll  11072  ccatcl  11136  swrdclg  11190  caucvgrelemcau  11499  caucvgre  11500  cvg1nlemf  11502  cvg1nlemcau  11503  cvg1nlemres  11504  recvguniqlem  11513  resqrexlemdecn  11531  resqrexlemcalc3  11535  resqrexlemnmsq  11536  resqrexlemnm  11537  resqrexlemcvg  11538  resqrexlemoverl  11540  resqrexlemglsq  11541  resqrexlemga  11542  clim2ser  11856  clim2ser2  11857  climrecvg1n  11867  climcvg1nlem  11868  serf0  11871  sumeq2  11878  fsum3cvg  11897  summodclem2a  11900  fsum3  11906  fisumss  11911  fsumcl2lem  11917  fsumadd  11925  fsummulc2  11967  fsumrelem  11990  isumshft  12009  cvgratnnlemseq  12045  cvgratnnlemrate  12049  clim2prod  12058  clim2divap  12059  prodfrecap  12065  prodfdivap  12066  ntrivcvgap  12067  prodeq2  12076  fproddccvg  12091  prodmodclem3  12094  prodmodclem2a  12095  fprodseq  12102  fprodssdc  12109  fprodmul  12110  effsumlt  12211  nninfctlemfo  12569  nn0seqcvgd  12571  ialgrlem1st  12572  eulerthlemrprm  12759  eulerthlema  12760  eulerthlemh  12761  pcmpt2  12875  pcmptdvds  12876  1arithlem4  12897  1arith  12898  ennnfonelemdc  12978  ennnfonelemjn  12981  ennnfonelemg  12982  ennnfonelemp1  12985  ennnfonelemom  12987  ennnfonelemhdmp1  12988  ennnfonelemss  12989  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ennnfonelemex  12993  ennnfonelemhom  12994  ennnfonelemnn0  13001  ennnfonelemim  13003  ctinfomlemom  13006  ctiunctlemudc  13016  ctiunctlemf  13017  ctiunctlemfo  13018  ssnnctlemct  13025  nninfdclemp1  13029  nninfdclemlt  13030  imasmnd2  13493  mhmf1o  13511  mhmco  13531  gsumfzcl  13540  isgrpinv  13595  pwssub  13654  imasgrp2  13655  mhmid  13660  mhmmnd  13661  ghmgrp  13663  mulgval  13667  mulgfng  13669  mulgnnsubcl  13679  ghmid  13794  ghminv  13795  ghmmulg  13801  ghmnsgpreima  13814  ghmeqker  13816  ghmf1  13818  kerf1ghm  13819  ghmf1o  13820  imasring  14035  rhmopp  14148  lspcl  14363  znidomb  14630  znrrg  14632  psrbaglesuppg  14644  psrbagfi  14645  mplsubgfilemcl  14671  iscnp4  14900  cnptopco  14904  lmtopcnp  14932  upxp  14954  uptx  14956  txlm  14961  comet  15181  metcnp3  15193  metcnp  15194  metcnp2  15195  metcnpi3  15199  elcncf2  15256  cncfco  15273  ivthreinc  15327  limcimolemlt  15346  cnplimcim  15349  cnplimclemle  15350  cnplimclemr  15351  limccnpcntop  15357  dvlemap  15362  dvcnp2cntop  15381  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvcjbr  15390  dvef  15409  plyaddlem1  15429  plymullem1  15430  plycoeid3  15439  plycolemc  15440  plycjlemc  15442  plycj  15443  plycn  15444  plyrecj  15445  dvply1  15447  dvply2g  15448  lgsval  15691  lgscllem  15694  lgsval2lem  15697  lgsval4a  15709  lgsneg  15711  lgsdir  15722  lgsdilem2  15723  lgsdi  15724  lgsne0  15725  lgseisenlem3  15759  lgseisenlem4  15760  wlkvtxm  16061  wlkvtxiedg  16066  wlkvtxiedgg  16067  upgriswlkdc  16081  1dom1el  16378  3dom  16381  2omap  16388  pwle2  16393  subctctexmid  16395  nnsf  16401  peano4nninf  16402  nninfalllem1  16404  nninfsellemdc  16406  nninfsellemeq  16410  nninfsellemqall  16411  nninfsellemeqinf  16412  nninfomnilem  16414  nnnninfex  16418  nninfnfiinf  16419  isomninnlem  16428  trilpolemeq1  16438  trilpolemlt1  16439  iswomninnlem  16447  iswomni0  16449  ismkvnnlem  16450  nconstwlpolemgt0  16462  nconstwlpolem  16463