Theorem ffvelcdmda 5790

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 5788	. 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 2202   -->wf 5329   ` cfv 5333

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-fv 5341

This theorem is referenced by:  ffvelcdmd  5791  f1ocnvdm  5932  foeqcnvco  5941  f1oiso2  5978  offeq  6258  suppssof1  6262  ofco  6263  caofref  6269  caofinvl  6270  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  caofcom  6275  caofrss  6276  caoftrn  6277  caofdig  6278  suppssrst  6439  suppssrgst  6440  suppofss1dcl  6442  suppofss2dcl  6443  smofvon2dm  6505  smofvon  6508  pw2f1odclem  7063  mapxpen  7077  xpmapenlem  7078  en2eqpr  7142  supisoex  7268  ordiso2  7294  omp1eomlem  7353  ctssdccl  7370  ctssdc  7372  enumctlemm  7373  enomnilem  7397  fodjuomnilemdc  7403  ismkvnex  7414  enmkvlem  7420  enwomnilem  7428  nninfwlporlemd  7431  nninfwlporlem  7432  nninfwlpoimlemginf  7435  cc3  7547  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  caucvgprlemladdrl  7958  caucvgprprlemopu  7979  caucvgprprlemexbt  7986  caucvgprprlemexb  7987  caucvgsrlemcl  8069  caucvgsrlemfv  8071  caucvgsrlemcau  8073  caucvgsrlembound  8074  caucvgsrlemoffval  8076  caucvgsrlemofff  8077  caucvgsrlemoffgt1  8079  caucvgsrlemoffres  8080  caucvgsr  8082  axcaucvglemcl  8175  ofnegsub  9201  frecuzrdgfunlem  10744  monoord2  10811  seq3f1o  10842  seqf1oglem2  10845  seqf1og  10846  seq3homo  10852  seqfeq3  10854  zfz1isolemiso  11166  seq3coll  11169  wrdsymbcl  11193  ccatcl  11236  resqrexlemfp1  11649  resqrexlemover  11650  resqrexlemdec  11651  resqrexlemlo  11653  resqrexlemcalc1  11654  resqrexlemcalc2  11655  resqrexlemcalc3  11656  resqrexlemgt0  11660  resqrexlemsqa  11664  clim2ser  11977  clim2ser2  11978  isermulc2  11980  iserle  11982  climserle  11985  climrecvg1n  11988  climcvg1nlem  11989  summodclem3  12021  summodclem2a  12022  fsumgcl  12027  fsum3  12028  fsumf1o  12031  isumss  12032  fisumss  12033  fsumcl2lem  12039  fsumadd  12047  isumclim3  12064  isummulc2  12067  isumrecl  12070  isumadd  12072  fsummulc2  12089  iserabs  12116  cvgcmpub  12117  isumshft  12131  isumsplit  12132  mertensabs  12178  clim2prod  12180  clim2divap  12181  prodfap0  12186  prodfdivap  12188  prodmodclem3  12216  prodmodclem2a  12217  fprodseq  12224  fprodf1o  12229  prodssdc  12230  fprodssdc  12231  fprodmul  12232  efcj  12314  nninfctlemfo  12691  nn0seqcvgd  12693  algrp1  12698  alginv  12699  algcvg  12700  algcvga  12703  algfx  12704  eucalgcvga  12710  eulerthlem1  12879  eulerthlemh  12883  eulerthlemth  12884  pcmptcl  12995  pcmpt  12996  1arithlem4  13019  nninfdclemf1  13153  prdsplusgsgrpcl  13577  prdssgrpd  13578  prdsplusgcl  13609  prdsidlem  13610  prdsmndd  13611  gsumwsubmcl  13659  gsumwmhm  13661  grpinvcl  13711  prdsinvlem  13771  pwsinvg  13775  pwssub  13776  mhmmulg  13830  ghminv  13917  gsumfzreidx  14004  gsumfzsubmcl  14005  gsumfzmptfidmadd  14006  gsumfzmhm  14010  rhmdvdsr  14270  rrgsupp  14361  psrbagcon  14772  psrbagconf1o  14774  psrlinv  14785  psr1clfi  14789  mplsubgfilemcl  14800  cnptoprest2  15051  lmss  15057  txcnmpt  15084  txlm  15090  lmcn2  15091  psmetxrge0  15143  metcnp  15323  climcncf  15395  negfcncf  15417  ivthdec  15455  ivthreinc  15456  dvcnp2cntop  15510  dvaddxxbr  15512  dvimulf  15517  dvcj  15520  dvfre  15521  elply2  15546  plyaddlem1  15558  plymullem1  15559  plycolemc  15569  plyco  15570  dvply2g  15577  lgscllem  15826  lgsfle1  15828  lgsval4a  15841  lgsneg  15843  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  uhgrss  16016  uhgrm  16019  upgrss  16040  upgrm  16041  upgr1or2  16042  umgredg2en  16050  lfgredg2dom  16073  usgrss  16118  depindlem1  16447  depindlem2  16448  pw1map  16717  nninfall  16735  nninffeq  16746  refeq  16756  trilpolemclim  16768  trilpolemcl  16769  trilpolemisumle  16770  trilpolemeq1  16772  iswomni0  16784