Theorem ffvelcdmda 5738

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 5736	. 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 2178   -->wf 5286   ` cfv 5290

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-sbc 3006  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-iota 5251  df-fun 5292  df-fn 5293  df-f 5294  df-fv 5298

This theorem is referenced by:  ffvelcdmd  5739  f1ocnvdm  5873  foeqcnvco  5882  f1oiso2  5919  offeq  6195  suppssof1  6199  ofco  6200  caofref  6206  caofinvl  6207  caofid0l  6208  caofid0r  6209  caofid1  6210  caofid2  6211  caofcom  6212  caofrss  6213  caoftrn  6214  caofdig  6215  smofvon2dm  6405  smofvon  6408  pw2f1odclem  6956  mapxpen  6970  xpmapenlem  6971  en2eqpr  7030  supisoex  7137  ordiso2  7163  omp1eomlem  7222  ctssdccl  7239  ctssdc  7241  enumctlemm  7242  enomnilem  7266  fodjuomnilemdc  7272  ismkvnex  7283  enmkvlem  7289  enwomnilem  7297  nninfwlporlemd  7300  nninfwlporlem  7301  nninfwlpoimlemginf  7304  cc3  7415  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprlemladdrl  7826  caucvgprprlemopu  7847  caucvgprprlemexbt  7854  caucvgprprlemexb  7855  caucvgsrlemcl  7937  caucvgsrlemfv  7939  caucvgsrlemcau  7941  caucvgsrlembound  7942  caucvgsrlemoffval  7944  caucvgsrlemofff  7945  caucvgsrlemoffgt1  7947  caucvgsrlemoffres  7948  caucvgsr  7950  axcaucvglemcl  8043  ofnegsub  9070  frecuzrdgfunlem  10601  monoord2  10668  seq3f1o  10699  seqf1oglem2  10702  seqf1og  10703  seq3homo  10709  seqfeq3  10711  zfz1isolemiso  11021  seq3coll  11024  wrdsymbcl  11045  ccatcl  11087  resqrexlemfp1  11435  resqrexlemover  11436  resqrexlemdec  11437  resqrexlemlo  11439  resqrexlemcalc1  11440  resqrexlemcalc2  11441  resqrexlemcalc3  11442  resqrexlemgt0  11446  resqrexlemsqa  11450  clim2ser  11763  clim2ser2  11764  isermulc2  11766  iserle  11768  climserle  11771  climrecvg1n  11774  climcvg1nlem  11775  summodclem3  11806  summodclem2a  11807  fsumgcl  11812  fsum3  11813  fsumf1o  11816  isumss  11817  fisumss  11818  fsumcl2lem  11824  fsumadd  11832  isumclim3  11849  isummulc2  11852  isumrecl  11855  isumadd  11857  fsummulc2  11874  iserabs  11901  cvgcmpub  11902  isumshft  11916  isumsplit  11917  mertensabs  11963  clim2prod  11965  clim2divap  11966  prodfap0  11971  prodfdivap  11973  prodmodclem3  12001  prodmodclem2a  12002  fprodseq  12009  fprodf1o  12014  prodssdc  12015  fprodssdc  12016  fprodmul  12017  efcj  12099  nninfctlemfo  12476  nn0seqcvgd  12478  algrp1  12483  alginv  12484  algcvg  12485  algcvga  12488  algfx  12489  eucalgcvga  12495  eulerthlem1  12664  eulerthlemh  12668  eulerthlemth  12669  pcmptcl  12780  pcmpt  12781  1arithlem4  12804  nninfdclemf1  12938  prdsplusgsgrpcl  13361  prdssgrpd  13362  prdsplusgcl  13393  prdsidlem  13394  prdsmndd  13395  gsumwsubmcl  13443  gsumwmhm  13445  grpinvcl  13495  prdsinvlem  13555  pwsinvg  13559  pwssub  13560  mhmmulg  13614  ghminv  13701  gsumfzreidx  13788  gsumfzsubmcl  13789  gsumfzmptfidmadd  13790  gsumfzmhm  13794  rhmdvdsr  14052  psrlinv  14561  psr1clfi  14565  mplsubgfilemcl  14576  cnptoprest2  14827  lmss  14833  txcnmpt  14860  txlm  14866  lmcn2  14867  psmetxrge0  14919  metcnp  15099  climcncf  15171  negfcncf  15193  ivthdec  15231  ivthreinc  15232  dvcnp2cntop  15286  dvaddxxbr  15288  dvimulf  15293  dvcj  15296  dvfre  15297  elply2  15322  plyaddlem1  15334  plymullem1  15335  plycolemc  15345  plyco  15346  dvply2g  15353  lgscllem  15599  lgsfle1  15601  lgsval4a  15614  lgsneg  15616  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  uhgrss  15786  uhgrm  15789  upgrss  15810  upgrm  15811  upgr1or2  15812  umgredg2en  15820  lfgredg2dom  15838  pw1map  16134  nninfall  16148  nninffeq  16159  refeq  16169  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  iswomni0  16192