Theorem ffvelcdmda 5843

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 5841	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   -->wf 5373   ` cfv 5377

This proof depends on 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 4249  ax-pow 4311  ax-pr 4346

This proof 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 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-fv 5385

This theorem is used by:  ffvelcdmd  5844  f1ocnvdm  5987  foeqcnvco  5996  f1oiso2  6033  offeq  6316  suppssof1  6320  ofco  6321  caofref  6327  caofinvl  6328  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  caofcom  6333  caofrss  6334  caoftrn  6335  caofdig  6336  suppssrst  6501  suppssrgst  6502  suppofss1dcl  6504  suppofss2dcl  6505  smofvon2dm  6567  smofvon  6570  pw2f1odclem  7134  mapxpen  7148  xpmapenlem  7149  en2eqpr  7214  supisoex  7350  ordiso2  7376  omp1eomlem  7435  ctssdccl  7452  ctssdc  7454  enumctlemm  7455  enomnilem  7479  fodjuomnilemdc  7485  ismkvnex  7496  enmkvlem  7502  enwomnilem  7510  nninfwlporlemd  7513  nninfwlporlem  7514  nninfwlpoimlemginf  7517  cc3  7635  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  caucvgprprlemopu  8067  caucvgprprlemexbt  8074  caucvgprprlemexb  8075  caucvgsrlemcl  8157  caucvgsrlemfv  8159  caucvgsrlemcau  8161  caucvgsrlembound  8162  caucvgsrlemoffval  8164  caucvgsrlemofff  8165  caucvgsrlemoffgt1  8167  caucvgsrlemoffres  8168  caucvgsr  8170  axcaucvglemcl  8263  ofnegsub  9295  frecuzrdgfunlem  10871  monoord2  10938  seq3f1o  10969  seqf1oglem2  10972  seqf1og  10973  seq3homo  10979  seqfeq3  10981  zfz1isolemiso  11307  seq3coll  11310  wrdsymbcl  11334  ccatcl  11377  resqrexlemfp1  11791  resqrexlemover  11792  resqrexlemdec  11793  resqrexlemlo  11795  resqrexlemcalc1  11796  resqrexlemcalc2  11797  resqrexlemcalc3  11798  resqrexlemgt0  11802  resqrexlemsqa  11806  clim2ser  12122  clim2ser2  12123  isermulc2  12125  iserle  12127  climserle  12130  climrecvg1n  12133  climcvg1nlem  12134  summodclem3  12166  summodclem2a  12167  fsumgcl  12172  fsum3  12173  fsumf1o  12176  isumss  12177  fisumss  12178  fsumcl2lem  12184  fsumadd  12192  isumclim3  12209  isummulc2  12212  isumrecl  12215  isumadd  12217  fsummulc2  12234  iserabs  12261  cvgcmpub  12262  isumshft  12276  isumsplit  12277  mertensabs  12323  clim2prod  12325  clim2divap  12326  prodfap0  12331  prodfdivap  12333  prodmodclem3  12361  prodmodclem2a  12362  fprodseq  12369  fprodf1o  12374  prodssdc  12375  fprodssdc  12376  fprodmul  12377  efcj  12459  nninfctlemfo  12836  nn0seqcvgd  12838  algrp1  12843  alginv  12844  algcvg  12845  algcvga  12848  algfx  12849  eucalgcvga  12855  eulerthlem1  13028  eulerthlemh  13032  eulerthlemth  13033  pcmptcl  13144  pcmpt  13145  1arithlem4  13168  nninfdclemf1  13395  gzsumwsubmcl  13854  gzsumwmhm  13856  grpinvcl  13906  mhmmulg  14019  ghminv  14106  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gsumf1ofi  14244  prdsplusgsgrpcl  14274  prdssgrpd  14275  prdsplusgcl  14276  prdsidlem  14277  prdsmndd  14278  prdsinvlem  14280  pwsinvg  14299  pwssub  14300  rhmdvdsr  14566  rrgsupp  14658  ascldimul  15115  psrbagcon  15146  psrbaglefifi  15147  psrbagconf1o  15149  psrlinv  15166  psr1clfi  15170  mplsubgfilemcl  15181  cnptoprest2  15432  lmss  15438  txcnmpt  15465  txlm  15471  lmcn2  15472  psmetxrge0  15524  metcnp  15704  climcncf  15776  negfcncf  15798  ivthdec  15836  ivthreinc  15837  dvcnp2cntop  15891  dvaddxxbr  15893  dvimulf  15898  dvcj  15901  dvfre  15902  elply2  15927  plyaddlem1  15939  plymullem1  15940  plycolemc  15950  plyco  15951  dvply2g  15958  bposlem5  16276  lgscllem  16292  lgsfle1  16294  lgsval4a  16307  lgsneg  16309  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  uhgrss  16482  uhgrm  16485  upgrss  16506  upgrm  16507  upgr1or2  16508  umgredg2en  16516  lfgredg2dom  16539  usgrss  16584  depindlem1  16913  depindlem2  16914  pw1map  17191  nninfall  17218  nninffeq  17229  refeq  17239  trilpolemclim  17252  trilpolemcl  17253  trilpolemisumle  17254  trilpolemeq1  17256  iswomni0  17268