Theorem ffvelcdmda 5697

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 5695	. 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 2167   -->wf 5254   ` cfv 5258

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-sbc 2990  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-opab 4095  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-fv 5266

This theorem is referenced by:  ffvelcdmd  5698  f1ocnvdm  5828  foeqcnvco  5837  f1oiso2  5874  offeq  6149  suppssof1  6153  ofco  6154  caofref  6159  caofinvl  6160  caofcom  6161  caofrss  6162  caoftrn  6163  caofdig  6164  smofvon2dm  6354  smofvon  6357  pw2f1odclem  6895  mapxpen  6909  xpmapenlem  6910  en2eqpr  6968  supisoex  7075  ordiso2  7101  omp1eomlem  7160  ctssdccl  7177  ctssdc  7179  enumctlemm  7180  enomnilem  7204  fodjuomnilemdc  7210  ismkvnex  7221  enmkvlem  7227  enwomnilem  7235  nninfwlporlemd  7238  nninfwlporlem  7239  nninfwlpoimlemginf  7242  cc3  7335  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  caucvgprprlemopu  7766  caucvgprprlemexbt  7773  caucvgprprlemexb  7774  caucvgsrlemcl  7856  caucvgsrlemfv  7858  caucvgsrlemcau  7860  caucvgsrlembound  7861  caucvgsrlemoffval  7863  caucvgsrlemofff  7864  caucvgsrlemoffgt1  7866  caucvgsrlemoffres  7867  caucvgsr  7869  axcaucvglemcl  7962  ofnegsub  8989  frecuzrdgfunlem  10511  monoord2  10578  seq3f1o  10609  seqf1oglem2  10612  seqf1og  10613  seq3homo  10619  seqfeq3  10621  zfz1isolemiso  10931  seq3coll  10934  wrdsymbcl  10949  resqrexlemfp1  11174  resqrexlemover  11175  resqrexlemdec  11176  resqrexlemlo  11178  resqrexlemcalc1  11179  resqrexlemcalc2  11180  resqrexlemcalc3  11181  resqrexlemgt0  11185  resqrexlemsqa  11189  clim2ser  11502  clim2ser2  11503  isermulc2  11505  iserle  11507  climserle  11510  climrecvg1n  11513  climcvg1nlem  11514  summodclem3  11545  summodclem2a  11546  fsumgcl  11551  fsum3  11552  fsumf1o  11555  isumss  11556  fisumss  11557  fsumcl2lem  11563  fsumadd  11571  isumclim3  11588  isummulc2  11591  isumrecl  11594  isumadd  11596  fsummulc2  11613  iserabs  11640  cvgcmpub  11641  isumshft  11655  isumsplit  11656  mertensabs  11702  clim2prod  11704  clim2divap  11705  prodfap0  11710  prodfdivap  11712  prodmodclem3  11740  prodmodclem2a  11741  fprodseq  11748  fprodf1o  11753  prodssdc  11754  fprodssdc  11755  fprodmul  11756  efcj  11838  nninfctlemfo  12207  nn0seqcvgd  12209  algrp1  12214  alginv  12215  algcvg  12216  algcvga  12219  algfx  12220  eucalgcvga  12226  eulerthlem1  12395  eulerthlemh  12399  eulerthlemth  12400  pcmptcl  12511  pcmpt  12512  1arithlem4  12535  nninfdclemf1  12669  gsumwsubmcl  13128  gsumwmhm  13130  grpinvcl  13180  mhmmulg  13293  ghminv  13380  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  rhmdvdsr  13731  cnptoprest2  14476  lmss  14482  txcnmpt  14509  txlm  14515  lmcn2  14516  psmetxrge0  14568  metcnp  14748  climcncf  14820  negfcncf  14842  ivthdec  14880  ivthreinc  14881  dvcnp2cntop  14935  dvaddxxbr  14937  dvimulf  14942  dvcj  14945  dvfre  14946  elply2  14971  plyaddlem1  14983  plymullem1  14984  plycolemc  14994  plyco  14995  dvply2g  15002  lgscllem  15248  lgsfle1  15250  lgsval4a  15263  lgsneg  15265  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  nninfall  15653  nninffeq  15664  refeq  15672  trilpolemclim  15680  trilpolemcl  15681  trilpolemisumle  15682  trilpolemeq1  15684  iswomni0  15695