Theorem ffvelcdmda 5770

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 5768	. 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  5771  f1ocnvdm  5905  foeqcnvco  5914  f1oiso2  5951  offeq  6232  suppssof1  6236  ofco  6237  caofref  6243  caofinvl  6244  caofid0l  6245  caofid0r  6246  caofid1  6247  caofid2  6248  caofcom  6249  caofrss  6250  caoftrn  6251  caofdig  6252  smofvon2dm  6442  smofvon  6445  pw2f1odclem  6995  mapxpen  7009  xpmapenlem  7010  en2eqpr  7069  supisoex  7176  ordiso2  7202  omp1eomlem  7261  ctssdccl  7278  ctssdc  7280  enumctlemm  7281  enomnilem  7305  fodjuomnilemdc  7311  ismkvnex  7322  enmkvlem  7328  enwomnilem  7336  nninfwlporlemd  7339  nninfwlporlem  7340  nninfwlpoimlemginf  7343  cc3  7454  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  caucvgprlemladdrl  7865  caucvgprprlemopu  7886  caucvgprprlemexbt  7893  caucvgprprlemexb  7894  caucvgsrlemcl  7976  caucvgsrlemfv  7978  caucvgsrlemcau  7980  caucvgsrlembound  7981  caucvgsrlemoffval  7983  caucvgsrlemofff  7984  caucvgsrlemoffgt1  7986  caucvgsrlemoffres  7987  caucvgsr  7989  axcaucvglemcl  8082  ofnegsub  9109  frecuzrdgfunlem  10641  monoord2  10708  seq3f1o  10739  seqf1oglem2  10742  seqf1og  10743  seq3homo  10749  seqfeq3  10751  zfz1isolemiso  11061  seq3coll  11064  wrdsymbcl  11085  ccatcl  11128  resqrexlemfp1  11520  resqrexlemover  11521  resqrexlemdec  11522  resqrexlemlo  11524  resqrexlemcalc1  11525  resqrexlemcalc2  11526  resqrexlemcalc3  11527  resqrexlemgt0  11531  resqrexlemsqa  11535  clim2ser  11848  clim2ser2  11849  isermulc2  11851  iserle  11853  climserle  11856  climrecvg1n  11859  climcvg1nlem  11860  summodclem3  11891  summodclem2a  11892  fsumgcl  11897  fsum3  11898  fsumf1o  11901  isumss  11902  fisumss  11903  fsumcl2lem  11909  fsumadd  11917  isumclim3  11934  isummulc2  11937  isumrecl  11940  isumadd  11942  fsummulc2  11959  iserabs  11986  cvgcmpub  11987  isumshft  12001  isumsplit  12002  mertensabs  12048  clim2prod  12050  clim2divap  12051  prodfap0  12056  prodfdivap  12058  prodmodclem3  12086  prodmodclem2a  12087  fprodseq  12094  fprodf1o  12099  prodssdc  12100  fprodssdc  12101  fprodmul  12102  efcj  12184  nninfctlemfo  12561  nn0seqcvgd  12563  algrp1  12568  alginv  12569  algcvg  12570  algcvga  12573  algfx  12574  eucalgcvga  12580  eulerthlem1  12749  eulerthlemh  12753  eulerthlemth  12754  pcmptcl  12865  pcmpt  12866  1arithlem4  12889  nninfdclemf1  13023  prdsplusgsgrpcl  13447  prdssgrpd  13448  prdsplusgcl  13479  prdsidlem  13480  prdsmndd  13481  gsumwsubmcl  13529  gsumwmhm  13531  grpinvcl  13581  prdsinvlem  13641  pwsinvg  13645  pwssub  13646  mhmmulg  13700  ghminv  13787  gsumfzreidx  13874  gsumfzsubmcl  13875  gsumfzmptfidmadd  13876  gsumfzmhm  13880  rhmdvdsr  14139  psrlinv  14648  psr1clfi  14652  mplsubgfilemcl  14663  cnptoprest2  14914  lmss  14920  txcnmpt  14947  txlm  14953  lmcn2  14954  psmetxrge0  15006  metcnp  15186  climcncf  15258  negfcncf  15280  ivthdec  15318  ivthreinc  15319  dvcnp2cntop  15373  dvaddxxbr  15375  dvimulf  15380  dvcj  15383  dvfre  15384  elply2  15409  plyaddlem1  15421  plymullem1  15422  plycolemc  15432  plyco  15433  dvply2g  15440  lgscllem  15686  lgsfle1  15688  lgsval4a  15701  lgsneg  15703  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  uhgrss  15875  uhgrm  15878  upgrss  15899  upgrm  15900  upgr1or2  15901  umgredg2en  15909  lfgredg2dom  15930  usgrss  15975  pw1map  16361  nninfall  16375  nninffeq  16386  refeq  16396  trilpolemclim  16404  trilpolemcl  16405  trilpolemisumle  16406  trilpolemeq1  16408  iswomni0  16419