Theorem ffvelcdmda 5772

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

Hypothesis

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

Assertion

Ref	Expression
ffvelcdmda	|- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )

Proof of Theorem ffvelcdmda

Step	Hyp	Ref	Expression
1		ffvelcdmd.1	. 2 |- ( ph -> F : A --> B )
2		ffvelcdm 5770	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )
3	1, 2	sylan 283	1 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   /\ wa 104   e. 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:  ffvelcdmd  5773  f1ocnvdm  5911  foeqcnvco  5920  f1oiso2  5957  offeq  6238  suppssof1  6242  ofco  6243  caofref  6249  caofinvl  6250  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  caofcom  6255  caofrss  6256  caoftrn  6257  caofdig  6258  smofvon2dm  6448  smofvon  6451  pw2f1odclem  7003  mapxpen  7017  xpmapenlem  7018  en2eqpr  7080  supisoex  7187  ordiso2  7213  omp1eomlem  7272  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  enomnilem  7316  fodjuomnilemdc  7322  ismkvnex  7333  enmkvlem  7339  enwomnilem  7347  nninfwlporlemd  7350  nninfwlporlem  7351  nninfwlpoimlemginf  7354  cc3  7465  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  caucvgprprlemopu  7897  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsrlemcau  7991  caucvgsrlembound  7992  caucvgsrlemoffval  7994  caucvgsrlemofff  7995  caucvgsrlemoffgt1  7997  caucvgsrlemoffres  7998  caucvgsr  8000  axcaucvglemcl  8093  ofnegsub  9120  frecuzrdgfunlem  10653  monoord2  10720  seq3f1o  10751  seqf1oglem2  10754  seqf1og  10755  seq3homo  10761  seqfeq3  10763  zfz1isolemiso  11074  seq3coll  11077  wrdsymbcl  11098  ccatcl  11141  resqrexlemfp1  11536  resqrexlemover  11537  resqrexlemdec  11538  resqrexlemlo  11540  resqrexlemcalc1  11541  resqrexlemcalc2  11542  resqrexlemcalc3  11543  resqrexlemgt0  11547  resqrexlemsqa  11551  clim2ser  11864  clim2ser2  11865  isermulc2  11867  iserle  11869  climserle  11872  climrecvg1n  11875  climcvg1nlem  11876  summodclem3  11907  summodclem2a  11908  fsumgcl  11913  fsum3  11914  fsumf1o  11917  isumss  11918  fisumss  11919  fsumcl2lem  11925  fsumadd  11933  isumclim3  11950  isummulc2  11953  isumrecl  11956  isumadd  11958  fsummulc2  11975  iserabs  12002  cvgcmpub  12003  isumshft  12017  isumsplit  12018  mertensabs  12064  clim2prod  12066  clim2divap  12067  prodfap0  12072  prodfdivap  12074  prodmodclem3  12102  prodmodclem2a  12103  fprodseq  12110  fprodf1o  12115  prodssdc  12116  fprodssdc  12117  fprodmul  12118  efcj  12200  nninfctlemfo  12577  nn0seqcvgd  12579  algrp1  12584  alginv  12585  algcvg  12586  algcvga  12589  algfx  12590  eucalgcvga  12596  eulerthlem1  12765  eulerthlemh  12769  eulerthlemth  12770  pcmptcl  12881  pcmpt  12882  1arithlem4  12905  nninfdclemf1  13039  prdsplusgsgrpcl  13463  prdssgrpd  13464  prdsplusgcl  13495  prdsidlem  13496  prdsmndd  13497  gsumwsubmcl  13545  gsumwmhm  13547  grpinvcl  13597  prdsinvlem  13657  pwsinvg  13661  pwssub  13662  mhmmulg  13716  ghminv  13803  gsumfzreidx  13890  gsumfzsubmcl  13891  gsumfzmptfidmadd  13892  gsumfzmhm  13896  rhmdvdsr  14155  psrlinv  14664  psr1clfi  14668  mplsubgfilemcl  14679  cnptoprest2  14930  lmss  14936  txcnmpt  14963  txlm  14969  lmcn2  14970  psmetxrge0  15022  metcnp  15202  climcncf  15274  negfcncf  15296  ivthdec  15334  ivthreinc  15335  dvcnp2cntop  15389  dvaddxxbr  15391  dvimulf  15396  dvcj  15399  dvfre  15400  elply2  15425  plyaddlem1  15437  plymullem1  15438  plycolemc  15448  plyco  15449  dvply2g  15456  lgscllem  15702  lgsfle1  15704  lgsval4a  15717  lgsneg  15719  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  uhgrss  15891  uhgrm  15894  upgrss  15915  upgrm  15916  upgr1or2  15917  umgredg2en  15925  lfgredg2dom  15946  usgrss  15991  pw1map  16448  nninfall  16463  nninffeq  16474  refeq  16484  trilpolemclim  16492  trilpolemcl  16493  trilpolemisumle  16494  trilpolemeq1  16496  iswomni0  16507