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  7251  ordiso2  7277  omp1eomlem  7336  ctssdccl  7353  ctssdc  7355  enumctlemm  7356  enomnilem  7380  fodjuomnilemdc  7386  ismkvnex  7397  enmkvlem  7403  enwomnilem  7411  nninfwlporlemd  7414  nninfwlporlem  7415  nninfwlpoimlemginf  7418  cc3  7530  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  caucvgprprlemopu  7962  caucvgprprlemexbt  7969  caucvgprprlemexb  7970  caucvgsrlemcl  8052  caucvgsrlemfv  8054  caucvgsrlemcau  8056  caucvgsrlembound  8057  caucvgsrlemoffval  8059  caucvgsrlemofff  8060  caucvgsrlemoffgt1  8062  caucvgsrlemoffres  8063  caucvgsr  8065  axcaucvglemcl  8158  ofnegsub  9185  frecuzrdgfunlem  10725  monoord2  10792  seq3f1o  10823  seqf1oglem2  10826  seqf1og  10827  seq3homo  10833  seqfeq3  10835  zfz1isolemiso  11147  seq3coll  11150  wrdsymbcl  11174  ccatcl  11217  resqrexlemfp1  11630  resqrexlemover  11631  resqrexlemdec  11632  resqrexlemlo  11634  resqrexlemcalc1  11635  resqrexlemcalc2  11636  resqrexlemcalc3  11637  resqrexlemgt0  11641  resqrexlemsqa  11645  clim2ser  11958  clim2ser2  11959  isermulc2  11961  iserle  11963  climserle  11966  climrecvg1n  11969  climcvg1nlem  11970  summodclem3  12002  summodclem2a  12003  fsumgcl  12008  fsum3  12009  fsumf1o  12012  isumss  12013  fisumss  12014  fsumcl2lem  12020  fsumadd  12028  isumclim3  12045  isummulc2  12048  isumrecl  12051  isumadd  12053  fsummulc2  12070  iserabs  12097  cvgcmpub  12098  isumshft  12112  isumsplit  12113  mertensabs  12159  clim2prod  12161  clim2divap  12162  prodfap0  12167  prodfdivap  12169  prodmodclem3  12197  prodmodclem2a  12198  fprodseq  12205  fprodf1o  12210  prodssdc  12211  fprodssdc  12212  fprodmul  12213  efcj  12295  nninfctlemfo  12672  nn0seqcvgd  12674  algrp1  12679  alginv  12680  algcvg  12681  algcvga  12684  algfx  12685  eucalgcvga  12691  eulerthlem1  12860  eulerthlemh  12864  eulerthlemth  12865  pcmptcl  12976  pcmpt  12977  1arithlem4  13000  nninfdclemf1  13134  prdsplusgsgrpcl  13558  prdssgrpd  13559  prdsplusgcl  13590  prdsidlem  13591  prdsmndd  13592  gsumwsubmcl  13640  gsumwmhm  13642  grpinvcl  13692  prdsinvlem  13752  pwsinvg  13756  pwssub  13757  mhmmulg  13811  ghminv  13898  gsumfzreidx  13985  gsumfzsubmcl  13986  gsumfzmptfidmadd  13987  gsumfzmhm  13991  rhmdvdsr  14251  psrbagcon  14752  psrbagconf1o  14754  psrlinv  14765  psr1clfi  14769  mplsubgfilemcl  14780  cnptoprest2  15031  lmss  15037  txcnmpt  15064  txlm  15070  lmcn2  15071  psmetxrge0  15123  metcnp  15303  climcncf  15375  negfcncf  15397  ivthdec  15435  ivthreinc  15436  dvcnp2cntop  15490  dvaddxxbr  15492  dvimulf  15497  dvcj  15500  dvfre  15501  elply2  15526  plyaddlem1  15538  plymullem1  15539  plycolemc  15549  plyco  15550  dvply2g  15557  lgscllem  15803  lgsfle1  15805  lgsval4a  15818  lgsneg  15820  lgsdir  15831  lgsdilem2  15832  lgsdi  15833  lgsne0  15834  uhgrss  15993  uhgrm  15996  upgrss  16017  upgrm  16018  upgr1or2  16019  umgredg2en  16027  lfgredg2dom  16050  usgrss  16095  depindlem1  16424  depindlem2  16425  pw1map  16694  nninfall  16712  nninffeq  16723  refeq  16733  trilpolemclim  16745  trilpolemcl  16746  trilpolemisumle  16747  trilpolemeq1  16749  iswomni0  16761