Theorem ffvelcdmda 5647

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 5645	. 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 2148   -->wf 5208   ` cfv 5212

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-fv 5220

This theorem is referenced by:  ffvelcdmd  5648  f1ocnvdm  5776  foeqcnvco  5785  f1oiso2  5822  offeq  6090  suppssof1  6094  ofco  6095  caofref  6098  caofinvl  6099  caofcom  6100  caofrss  6101  caoftrn  6102  smofvon2dm  6291  smofvon  6294  mapxpen  6842  xpmapenlem  6843  en2eqpr  6901  supisoex  7002  ordiso2  7028  omp1eomlem  7087  ctssdccl  7104  ctssdc  7106  enumctlemm  7107  enomnilem  7130  fodjuomnilemdc  7136  ismkvnex  7147  enmkvlem  7153  enwomnilem  7161  nninfwlporlemd  7164  nninfwlporlem  7165  nninfwlpoimlemginf  7168  cc3  7258  cauappcvgprlemladdru  7646  cauappcvgprlemladdrl  7647  caucvgprlemladdrl  7668  caucvgprprlemopu  7689  caucvgprprlemexbt  7696  caucvgprprlemexb  7697  caucvgsrlemcl  7779  caucvgsrlemfv  7781  caucvgsrlemcau  7783  caucvgsrlembound  7784  caucvgsrlemoffval  7786  caucvgsrlemofff  7787  caucvgsrlemoffgt1  7789  caucvgsrlemoffres  7790  caucvgsr  7792  axcaucvglemcl  7885  frecuzrdgfunlem  10405  monoord2  10463  seq3f1o  10490  seq3homo  10496  seqfeq3  10498  zfz1isolemiso  10803  seq3coll  10806  resqrexlemfp1  11002  resqrexlemover  11003  resqrexlemdec  11004  resqrexlemlo  11006  resqrexlemcalc1  11007  resqrexlemcalc2  11008  resqrexlemcalc3  11009  resqrexlemgt0  11013  resqrexlemsqa  11017  clim2ser  11329  clim2ser2  11330  isermulc2  11332  iserle  11334  climserle  11337  climrecvg1n  11340  climcvg1nlem  11341  summodclem3  11372  summodclem2a  11373  fsumgcl  11378  fsum3  11379  fsumf1o  11382  isumss  11383  fisumss  11384  fsumcl2lem  11390  fsumadd  11398  isumclim3  11415  isummulc2  11418  isumrecl  11421  isumadd  11423  fsummulc2  11440  iserabs  11467  cvgcmpub  11468  isumshft  11482  isumsplit  11483  mertensabs  11529  clim2prod  11531  clim2divap  11532  prodfap0  11537  prodfdivap  11539  prodmodclem3  11567  prodmodclem2a  11568  fprodseq  11575  fprodf1o  11580  prodssdc  11581  fprodssdc  11582  fprodmul  11583  efcj  11665  nn0seqcvgd  12024  algrp1  12029  alginv  12030  algcvg  12031  algcvga  12034  algfx  12035  eucalgcvga  12041  eulerthlem1  12210  eulerthlemh  12214  eulerthlemth  12215  pcmptcl  12323  pcmpt  12324  1arithlem4  12347  nninfdclemf1  12436  grpinvcl  12811  mhmmulg  12912  cnptoprest2  13407  lmss  13413  txcnmpt  13440  txlm  13446  lmcn2  13447  psmetxrge0  13499  metcnp  13679  climcncf  13738  negfcncf  13756  ivthdec  13789  dvcnp2cntop  13830  dvaddxxbr  13832  dvimulf  13837  dvcj  13840  dvfre  13841  lgscllem  14075  lgsfle1  14077  lgsval4a  14090  lgsneg  14092  lgsdir  14103  lgsdilem2  14104  lgsdi  14105  lgsne0  14106  nninfall  14414  nninffeq  14425  refeq  14432  trilpolemclim  14440  trilpolemcl  14441  trilpolemisumle  14442  trilpolemeq1  14444  iswomni0  14455