Theorem ffvelcdmda 5715

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 5713	. 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 2176   -->wf 5267   ` cfv 5271

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279

This theorem is referenced by:  ffvelcdmd  5716  f1ocnvdm  5850  foeqcnvco  5859  f1oiso2  5896  offeq  6172  suppssof1  6176  ofco  6177  caofref  6183  caofinvl  6184  caofid0l  6185  caofid0r  6186  caofid1  6187  caofid2  6188  caofcom  6189  caofrss  6190  caoftrn  6191  caofdig  6192  smofvon2dm  6382  smofvon  6385  pw2f1odclem  6931  mapxpen  6945  xpmapenlem  6946  en2eqpr  7004  supisoex  7111  ordiso2  7137  omp1eomlem  7196  ctssdccl  7213  ctssdc  7215  enumctlemm  7216  enomnilem  7240  fodjuomnilemdc  7246  ismkvnex  7257  enmkvlem  7263  enwomnilem  7271  nninfwlporlemd  7274  nninfwlporlem  7275  nninfwlpoimlemginf  7278  cc3  7380  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemladdrl  7791  caucvgprprlemopu  7812  caucvgprprlemexbt  7819  caucvgprprlemexb  7820  caucvgsrlemcl  7902  caucvgsrlemfv  7904  caucvgsrlemcau  7906  caucvgsrlembound  7907  caucvgsrlemoffval  7909  caucvgsrlemofff  7910  caucvgsrlemoffgt1  7912  caucvgsrlemoffres  7913  caucvgsr  7915  axcaucvglemcl  8008  ofnegsub  9035  frecuzrdgfunlem  10564  monoord2  10631  seq3f1o  10662  seqf1oglem2  10665  seqf1og  10666  seq3homo  10672  seqfeq3  10674  zfz1isolemiso  10984  seq3coll  10987  wrdsymbcl  11008  ccatcl  11049  resqrexlemfp1  11320  resqrexlemover  11321  resqrexlemdec  11322  resqrexlemlo  11324  resqrexlemcalc1  11325  resqrexlemcalc2  11326  resqrexlemcalc3  11327  resqrexlemgt0  11331  resqrexlemsqa  11335  clim2ser  11648  clim2ser2  11649  isermulc2  11651  iserle  11653  climserle  11656  climrecvg1n  11659  climcvg1nlem  11660  summodclem3  11691  summodclem2a  11692  fsumgcl  11697  fsum3  11698  fsumf1o  11701  isumss  11702  fisumss  11703  fsumcl2lem  11709  fsumadd  11717  isumclim3  11734  isummulc2  11737  isumrecl  11740  isumadd  11742  fsummulc2  11759  iserabs  11786  cvgcmpub  11787  isumshft  11801  isumsplit  11802  mertensabs  11848  clim2prod  11850  clim2divap  11851  prodfap0  11856  prodfdivap  11858  prodmodclem3  11886  prodmodclem2a  11887  fprodseq  11894  fprodf1o  11899  prodssdc  11900  fprodssdc  11901  fprodmul  11902  efcj  11984  nninfctlemfo  12361  nn0seqcvgd  12363  algrp1  12368  alginv  12369  algcvg  12370  algcvga  12373  algfx  12374  eucalgcvga  12380  eulerthlem1  12549  eulerthlemh  12553  eulerthlemth  12554  pcmptcl  12665  pcmpt  12666  1arithlem4  12689  nninfdclemf1  12823  prdsplusgsgrpcl  13246  prdssgrpd  13247  prdsplusgcl  13278  prdsidlem  13279  prdsmndd  13280  gsumwsubmcl  13328  gsumwmhm  13330  grpinvcl  13380  prdsinvlem  13440  pwsinvg  13444  pwssub  13445  mhmmulg  13499  ghminv  13586  gsumfzreidx  13673  gsumfzsubmcl  13674  gsumfzmptfidmadd  13675  gsumfzmhm  13679  rhmdvdsr  13937  psrlinv  14446  psr1clfi  14450  mplsubgfilemcl  14461  cnptoprest2  14712  lmss  14718  txcnmpt  14745  txlm  14751  lmcn2  14752  psmetxrge0  14804  metcnp  14984  climcncf  15056  negfcncf  15078  ivthdec  15116  ivthreinc  15117  dvcnp2cntop  15171  dvaddxxbr  15173  dvimulf  15178  dvcj  15181  dvfre  15182  elply2  15207  plyaddlem1  15219  plymullem1  15220  plycolemc  15230  plyco  15231  dvply2g  15238  lgscllem  15484  lgsfle1  15486  lgsval4a  15499  lgsneg  15501  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  nninfall  15946  nninffeq  15957  refeq  15967  trilpolemclim  15975  trilpolemcl  15976  trilpolemisumle  15977  trilpolemeq1  15979  iswomni0  15990