Theorem ffvelcdmd 5647

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypotheses

Ref	Expression
ffvelcdmd.1	|- ( ph -> F : A --> B )
ffvelcdmd.2	|- ( ph -> C e. A )

Assertion

Ref	Expression
ffvelcdmd	|- ( ph -> ( F ` C ) e. B )

Proof of Theorem ffvelcdmd

Step	Hyp	Ref	Expression
1		ffvelcdmd.2	. 2 |- ( ph -> C e. A )
2		ffvelcdmd.1	. . 3 |- ( ph -> F : A --> B )
3	2	ffvelcdmda 5646	. 2 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )
4	1, 3	mpdan 421	1 |- ( ph -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   e. wcel 2148   -->wf 5207   ` cfv 5211

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4205

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-id 4289  df-xp 4628  df-rel 4629  df-cnv 4630  df-co 4631  df-dm 4632  df-rn 4633  df-iota 5173  df-fun 5213  df-fn 5214  df-f 5215  df-fv 5219

This theorem is referenced by:  isotr  5810  caofinvl  6098  rdgon  6380  frecabcl  6393  phplem4dom  6855  fidceq  6862  dif1en  6872  fin0  6878  fin0or  6879  infm  6897  en2eqpr  6900  fidcenumlemrks  6945  fidcenumlemr  6947  supisoti  7002  ordiso2  7027  updjudhcoinlf  7072  updjudhcoinrg  7073  caseinl  7083  caseinr  7084  difinfsnlem  7091  difinfsn  7092  ctmlemr  7100  ctssdclemn0  7102  ctssdc  7105  enumctlemm  7106  enumct  7107  nnnninfeq2  7120  nninfisol  7124  enomnilem  7129  finomni  7131  ismkvnex  7146  enmkvlem  7152  enwomnilem  7160  nninfwlpoimlemg  7166  nninfwlpoimlemginf  7167  exmidfodomrlemr  7194  exmidfodomrlemrALT  7195  cauappcvgprlemm  7622  cauappcvgprlemdisj  7628  cauappcvgprlemloc  7629  cauappcvgprlemladdfu  7631  cauappcvgprlemladdru  7633  cauappcvgprlemladdrl  7634  cauappcvgprlem1  7636  cauappcvgprlem2  7637  caucvgprlemnkj  7643  caucvgprlemnbj  7644  caucvgprlemm  7645  caucvgprlemloc  7652  caucvgprlemladdfu  7654  caucvgprlemladdrl  7655  caucvgprlem1  7656  caucvgprlem2  7657  caucvgprprlemnkltj  7666  caucvgprprlemnkeqj  7667  caucvgprprlemnbj  7670  caucvgprprlemmu  7672  caucvgprprlemopl  7674  caucvgprprlemloc  7680  caucvgprprlemexbt  7683  caucvgprprlemexb  7684  caucvgprprlemaddq  7685  caucvgprprlem1  7686  caucvgprprlem2  7687  caucvgsrlemcau  7770  caucvgsrlemgt1  7772  caucvgsrlemoffcau  7775  caucvgsrlemoffres  7777  caucvgsr  7779  axcaucvglemval  7874  axcaucvglemcau  7875  axcaucvglemres  7876  fseq1p1m1  10067  4fvwrd4  10113  fvinim0ffz  10214  frecuzrdgg  10389  frecuzrdgsuctlem  10396  seq3val  10431  seqvalcd  10432  seq3p1  10435  seqp1cd  10439  ser3mono  10451  seq3split  10452  seq3caopr2  10455  iseqf1olemkle  10457  iseqf1olemklt  10458  iseqf1olemqcl  10459  iseqf1olemnab  10461  iseqf1olemmo  10465  iseqf1olemqk  10467  iseqf1olemjpcl  10468  iseqf1olemqpcl  10469  iseqf1olemfvp  10470  seq3f1olemqsumkj  10471  seq3f1olemqsumk  10472  seq3f1olemqsum  10473  seq3f1olemstep  10474  seq3f1oleml  10476  seq3f1o  10477  seq3z  10484  seq3distr  10486  ser3ge0  10490  ser3le  10491  exp3vallem  10494  exp3val  10495  bcval5  10714  hashfz1  10734  resunimafz0  10782  leisorel  10788  zfz1isolemiso  10790  seq3coll  10793  caucvgrelemcau  10960  caucvgre  10961  cvg1nlemf  10963  cvg1nlemcau  10964  cvg1nlemres  10965  recvguniqlem  10974  resqrexlemdecn  10992  resqrexlemcalc3  10996  resqrexlemnmsq  10997  resqrexlemnm  10998  resqrexlemcvg  10999  resqrexlemoverl  11001  resqrexlemglsq  11002  resqrexlemga  11003  clim2ser  11316  clim2ser2  11317  climrecvg1n  11327  climcvg1nlem  11328  serf0  11331  sumeq2  11338  fsum3cvg  11357  summodclem2a  11360  fsum3  11366  fisumss  11371  fsumcl2lem  11377  fsumadd  11385  fsummulc2  11427  fsumrelem  11450  isumshft  11469  cvgratnnlemseq  11505  cvgratnnlemrate  11509  clim2prod  11518  clim2divap  11519  prodfrecap  11525  prodfdivap  11526  ntrivcvgap  11527  prodeq2  11536  fproddccvg  11551  prodmodclem3  11554  prodmodclem2a  11555  fprodseq  11562  fprodssdc  11569  fprodmul  11570  effsumlt  11671  nn0seqcvgd  12011  ialgrlem1st  12012  eulerthlemrprm  12199  eulerthlema  12200  eulerthlemh  12201  pcmpt2  12312  pcmptdvds  12313  1arithlem4  12334  1arith  12335  ennnfonelemdc  12370  ennnfonelemjn  12373  ennnfonelemg  12374  ennnfonelemp1  12377  ennnfonelemom  12379  ennnfonelemhdmp1  12380  ennnfonelemss  12381  ennnfonelemkh  12383  ennnfonelemhf1o  12384  ennnfonelemex  12385  ennnfonelemhom  12386  ennnfonelemnn0  12393  ennnfonelemim  12395  ctinfomlemom  12398  ctiunctlemudc  12408  ctiunctlemf  12409  ctiunctlemfo  12410  ssnnctlemct  12417  nninfdclemp1  12421  nninfdclemlt  12422  mhmf1o  12738  mhmco  12751  isgrpinv  12803  mhmid  12855  mhmmnd  12856  ghmgrp  12858  mulgval  12862  mulgfng  12863  mulgnnsubcl  12871  iscnp4  13351  cnptopco  13355  lmtopcnp  13383  upxp  13405  uptx  13407  txlm  13412  comet  13632  metcnp3  13644  metcnp  13645  metcnp2  13646  metcnpi3  13650  elcncf2  13694  cncfco  13711  limcimolemlt  13766  cnplimcim  13769  cnplimclemle  13770  cnplimclemr  13771  limccnpcntop  13777  dvlemap  13782  dvcnp2cntop  13796  dvaddxxbr  13798  dvmulxxbr  13799  dvcoapbr  13804  dvcjbr  13805  dvef  13821  lgsval  14038  lgscllem  14041  lgsval2lem  14044  lgsval4a  14056  lgsneg  14058  lgsdir  14069  lgsdilem2  14070  lgsdi  14071  lgsne0  14072  pwle2  14370  subctctexmid  14373  nnsf  14377  peano4nninf  14378  nninfalllem1  14380  nninfsellemdc  14382  nninfsellemeq  14386  nninfsellemqall  14387  nninfsellemeqinf  14388  nninfomnilem  14390  isomninnlem  14401  trilpolemeq1  14411  trilpolemlt1  14412  iswomninnlem  14420  iswomni0  14422  ismkvnnlem  14423  nconstwlpolemgt0  14434  nconstwlpolem  14435