Theorem ffvelcdmda 5694

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 5692	. 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 2164   -->wf 5251   ` cfv 5255

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-sbc 2987  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-rn 4671  df-iota 5216  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263

This theorem is referenced by:  ffvelcdmd  5695  f1ocnvdm  5825  foeqcnvco  5834  f1oiso2  5871  offeq  6146  suppssof1  6150  ofco  6151  caofref  6156  caofinvl  6157  caofcom  6158  caofrss  6159  caoftrn  6160  caofdig  6161  smofvon2dm  6351  smofvon  6354  pw2f1odclem  6892  mapxpen  6906  xpmapenlem  6907  en2eqpr  6965  supisoex  7070  ordiso2  7096  omp1eomlem  7155  ctssdccl  7172  ctssdc  7174  enumctlemm  7175  enomnilem  7199  fodjuomnilemdc  7205  ismkvnex  7216  enmkvlem  7222  enwomnilem  7230  nninfwlporlemd  7233  nninfwlporlem  7234  nninfwlpoimlemginf  7237  cc3  7330  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  caucvgprprlemopu  7761  caucvgprprlemexbt  7768  caucvgprprlemexb  7769  caucvgsrlemcl  7851  caucvgsrlemfv  7853  caucvgsrlemcau  7855  caucvgsrlembound  7856  caucvgsrlemoffval  7858  caucvgsrlemofff  7859  caucvgsrlemoffgt1  7861  caucvgsrlemoffres  7862  caucvgsr  7864  axcaucvglemcl  7957  ofnegsub  8983  frecuzrdgfunlem  10493  monoord2  10560  seq3f1o  10591  seqf1oglem2  10594  seqf1og  10595  seq3homo  10601  seqfeq3  10603  zfz1isolemiso  10913  seq3coll  10916  wrdsymbcl  10931  resqrexlemfp1  11156  resqrexlemover  11157  resqrexlemdec  11158  resqrexlemlo  11160  resqrexlemcalc1  11161  resqrexlemcalc2  11162  resqrexlemcalc3  11163  resqrexlemgt0  11167  resqrexlemsqa  11171  clim2ser  11483  clim2ser2  11484  isermulc2  11486  iserle  11488  climserle  11491  climrecvg1n  11494  climcvg1nlem  11495  summodclem3  11526  summodclem2a  11527  fsumgcl  11532  fsum3  11533  fsumf1o  11536  isumss  11537  fisumss  11538  fsumcl2lem  11544  fsumadd  11552  isumclim3  11569  isummulc2  11572  isumrecl  11575  isumadd  11577  fsummulc2  11594  iserabs  11621  cvgcmpub  11622  isumshft  11636  isumsplit  11637  mertensabs  11683  clim2prod  11685  clim2divap  11686  prodfap0  11691  prodfdivap  11693  prodmodclem3  11721  prodmodclem2a  11722  fprodseq  11729  fprodf1o  11734  prodssdc  11735  fprodssdc  11736  fprodmul  11737  efcj  11819  nninfctlemfo  12180  nn0seqcvgd  12182  algrp1  12187  alginv  12188  algcvg  12189  algcvga  12192  algfx  12193  eucalgcvga  12199  eulerthlem1  12368  eulerthlemh  12372  eulerthlemth  12373  pcmptcl  12483  pcmpt  12484  1arithlem4  12507  nninfdclemf1  12612  gsumwsubmcl  13071  gsumwmhm  13073  grpinvcl  13123  mhmmulg  13236  ghminv  13323  gsumfzreidx  13410  gsumfzsubmcl  13411  gsumfzmptfidmadd  13412  gsumfzmhm  13416  rhmdvdsr  13674  cnptoprest2  14419  lmss  14425  txcnmpt  14452  txlm  14458  lmcn2  14459  psmetxrge0  14511  metcnp  14691  climcncf  14763  negfcncf  14785  ivthdec  14823  ivthreinc  14824  dvcnp2cntop  14878  dvaddxxbr  14880  dvimulf  14885  dvcj  14888  dvfre  14889  elply2  14914  plyaddlem1  14926  plymullem1  14927  plycolemc  14936  plyco  14937  lgscllem  15164  lgsfle1  15166  lgsval4a  15179  lgsneg  15181  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  nninfall  15569  nninffeq  15580  refeq  15588  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  iswomni0  15611