Theorem ffvelcdmda 5834

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 5832	. 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 2209   -->wf 5368   ` cfv 5372

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306  ax-pr 4341

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-opab 4188  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-fv 5380

This theorem is referenced by:  ffvelcdmd  5835  f1ocnvdm  5977  foeqcnvco  5986  f1oiso2  6023  offeq  6306  suppssof1  6310  ofco  6311  caofref  6317  caofinvl  6318  caofid0l  6319  caofid0r  6320  caofid1  6321  caofid2  6322  caofcom  6323  caofrss  6324  caoftrn  6325  caofdig  6326  suppssrst  6491  suppssrgst  6492  suppofss1dcl  6494  suppofss2dcl  6495  smofvon2dm  6557  smofvon  6560  pw2f1odclem  7124  mapxpen  7138  xpmapenlem  7139  en2eqpr  7204  supisoex  7339  ordiso2  7365  omp1eomlem  7424  ctssdccl  7441  ctssdc  7443  enumctlemm  7444  enomnilem  7468  fodjuomnilemdc  7474  ismkvnex  7485  enmkvlem  7491  enwomnilem  7499  nninfwlporlemd  7502  nninfwlporlem  7503  nninfwlpoimlemginf  7506  cc3  7624  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  caucvgprprlemopu  8056  caucvgprprlemexbt  8063  caucvgprprlemexb  8064  caucvgsrlemcl  8146  caucvgsrlemfv  8148  caucvgsrlemcau  8150  caucvgsrlembound  8151  caucvgsrlemoffval  8153  caucvgsrlemofff  8154  caucvgsrlemoffgt1  8156  caucvgsrlemoffres  8157  caucvgsr  8159  axcaucvglemcl  8252  ofnegsub  9282  frecuzrdgfunlem  10834  monoord2  10901  seq3f1o  10932  seqf1oglem2  10935  seqf1og  10936  seq3homo  10942  seqfeq3  10944  zfz1isolemiso  11269  seq3coll  11272  wrdsymbcl  11296  ccatcl  11339  resqrexlemfp1  11753  resqrexlemover  11754  resqrexlemdec  11755  resqrexlemlo  11757  resqrexlemcalc1  11758  resqrexlemcalc2  11759  resqrexlemcalc3  11760  resqrexlemgt0  11764  resqrexlemsqa  11768  clim2ser  12081  clim2ser2  12082  isermulc2  12084  iserle  12086  climserle  12089  climrecvg1n  12092  climcvg1nlem  12093  summodclem3  12125  summodclem2a  12126  fsumgcl  12131  fsum3  12132  fsumf1o  12135  isumss  12136  fisumss  12137  fsumcl2lem  12143  fsumadd  12151  isumclim3  12168  isummulc2  12171  isumrecl  12174  isumadd  12176  fsummulc2  12193  iserabs  12220  cvgcmpub  12221  isumshft  12235  isumsplit  12236  mertensabs  12282  clim2prod  12284  clim2divap  12285  prodfap0  12290  prodfdivap  12292  prodmodclem3  12320  prodmodclem2a  12321  fprodseq  12328  fprodf1o  12333  prodssdc  12334  fprodssdc  12335  fprodmul  12336  efcj  12418  nninfctlemfo  12795  nn0seqcvgd  12797  algrp1  12802  alginv  12803  algcvg  12804  algcvga  12807  algfx  12808  eucalgcvga  12814  eulerthlem1  12983  eulerthlemh  12987  eulerthlemth  12988  pcmptcl  13099  pcmpt  13100  1arithlem4  13123  nninfdclemf1  13321  gzsumwsubmcl  13778  gzsumwmhm  13780  grpinvcl  13830  mhmmulg  13943  ghminv  14030  gzsumreidx  14118  gzsumsubmcl  14119  gzsummhm  14122  gsumf1ofi  14137  prdsplusgsgrpcl  14167  prdssgrpd  14168  prdsplusgcl  14169  prdsidlem  14170  prdsmndd  14171  prdsinvlem  14173  pwsinvg  14192  pwssub  14193  rhmdvdsr  14455  rrgsupp  14547  psrbagcon  14985  psrbagconf1o  14987  psrlinv  14998  psr1clfi  15002  mplsubgfilemcl  15013  cnptoprest2  15264  lmss  15270  txcnmpt  15297  txlm  15303  lmcn2  15304  psmetxrge0  15356  metcnp  15536  climcncf  15608  negfcncf  15630  ivthdec  15668  ivthreinc  15669  dvcnp2cntop  15723  dvaddxxbr  15725  dvimulf  15730  dvcj  15733  dvfre  15734  elply2  15759  plyaddlem1  15771  plymullem1  15772  plycolemc  15782  plyco  15783  dvply2g  15790  lgscllem  16040  lgsfle1  16042  lgsval4a  16055  lgsneg  16057  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  uhgrss  16230  uhgrm  16233  upgrss  16254  upgrm  16255  upgr1or2  16256  umgredg2en  16264  lfgredg2dom  16287  usgrss  16332  depindlem1  16661  depindlem2  16662  pw1map  16939  nninfall  16957  nninffeq  16968  refeq  16978  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  iswomni0  17006