Theorem ffvelcdmda 5846

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 5844	. 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 5376   ` cfv 5380

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 4251  ax-pow 4313  ax-pr 4348

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 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-fv 5388

This theorem is used by:  ffvelcdmd  5847  f1ocnvdm  5990  foeqcnvco  5999  f1oiso2  6036  offeq  6320  suppssof1  6324  ofco  6325  caofref  6331  caofinvl  6332  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  caofcom  6337  caofrss  6338  caoftrn  6339  caofdig  6340  suppssrst  6505  suppssrgst  6506  suppofss1dcl  6508  suppofss2dcl  6509  smofvon2dm  6571  smofvon  6574  pw2f1odclem  7138  mapxpen  7152  xpmapenlem  7153  en2eqpr  7218  supisoex  7355  ordiso2  7381  omp1eomlem  7440  ctssdccl  7457  ctssdc  7459  enumctlemm  7460  enomnilem  7484  fodjuomnilemdc  7490  ismkvnex  7501  enmkvlem  7507  enwomnilem  7515  nninfwlporlemd  7518  nninfwlporlem  7519  nninfwlpoimlemginf  7522  cc3  7640  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgprprlemopu  8072  caucvgprprlemexbt  8079  caucvgprprlemexb  8080  caucvgsrlemcl  8162  caucvgsrlemfv  8164  caucvgsrlemcau  8166  caucvgsrlembound  8167  caucvgsrlemoffval  8169  caucvgsrlemofff  8170  caucvgsrlemoffgt1  8172  caucvgsrlemoffres  8173  caucvgsr  8175  axcaucvglemcl  8268  ofsubeq0  9300  ofnegsub  9301  frecuzrdgfunlem  10877  monoord2  10944  seq3f1o  10975  seqf1oglem2  10978  seqf1og  10979  seq3homo  10985  seqfeq3  10987  zfz1isolemiso  11313  seq3coll  11316  wrdsymbcl  11340  ccatcl  11383  resqrexlemfp1  11797  resqrexlemover  11798  resqrexlemdec  11799  resqrexlemlo  11801  resqrexlemcalc1  11802  resqrexlemcalc2  11803  resqrexlemcalc3  11804  resqrexlemgt0  11808  resqrexlemsqa  11812  clim2ser  12128  clim2ser2  12129  isermulc2  12131  iserle  12133  climserle  12136  climrecvg1n  12139  climcvg1nlem  12140  summodclem3  12172  summodclem2a  12173  fsumgcl  12178  fsum3  12179  fsumf1o  12182  isumss  12183  fisumss  12184  fsumcl2lem  12190  fsumadd  12198  isumclim3  12215  isummulc2  12218  isumrecl  12221  isumadd  12223  fsummulc2  12240  iserabs  12267  cvgcmpub  12268  isumshft  12282  isumsplit  12283  mertensabs  12329  clim2prod  12331  clim2divap  12332  prodfap0  12337  prodfdivap  12339  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodmul  12383  efcj  12465  nninfctlemfo  12842  nn0seqcvgd  12844  algrp1  12849  alginv  12850  algcvg  12851  algcvga  12854  algfx  12855  eucalgcvga  12861  eulerthlem1  13034  eulerthlemh  13038  eulerthlemth  13039  pcmptcl  13150  pcmpt  13151  1arithlem4  13174  nninfdclemf1  13401  gzsumwsubmcl  13860  gzsumwmhm  13862  grpinvcl  13912  mhmmulg  14025  ghminv  14112  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gsumf1ofi  14250  gsumsplitfi  14256  gsum2dfilem1  14271  gsum2dfilem2  14272  prdsplusgsgrpcl  14297  prdssgrpd  14298  prdsplusgcl  14299  prdsidlem  14300  prdsmndd  14301  prdsinvlem  14303  pwsinvg  14322  pwssub  14323  rhmdvdsr  14591  rrgsupp  14683  ascldimul  15140  psrbagcon  15171  psrbaglefifi  15172  psrbagconf1o  15174  gsumbagdiaglem  15175  psrass1filem  15177  psrlinv  15194  psr1clfi  15198  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  psrdifi  15202  psrdirfi  15203  mplsubgfilemcl  15215  cnptoprest2  15466  lmss  15472  txcnmpt  15499  txlm  15505  lmcn2  15506  psmetxrge0  15558  metcnp  15738  climcncf  15810  negfcncf  15832  ivthdec  15870  ivthreinc  15871  dvcnp2cntop  15925  dvaddxxbr  15927  dvimulf  15932  dvcj  15935  dvfre  15936  elply2  15961  plyaddlem1  15973  plymullem1  15974  plycolemc  15984  plyco  15985  dvply2g  15992  bposlem5  16315  lgscllem  16331  lgsfle1  16333  lgsval4a  16346  lgsneg  16348  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  uhgrss  16521  uhgrm  16524  upgrss  16545  upgrm  16546  upgr1or2  16547  umgredg2en  16555  lfgredg2dom  16578  usgrss  16623  depindlem1  16952  depindlem2  16953  pw1map  17230  nninfall  17258  nninffeq  17269  refeq  17279  trilpolemclim  17292  trilpolemcl  17293  trilpolemisumle  17294  trilpolemeq1  17296  iswomni0  17308