Theorem ffvelcdmd 5698

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypotheses

Ref	Expression
ffvelcdmd.1	|- ( ph -> F : A --> B )
ffvelcdmd.2	|- ( ph -> C e. A )

Assertion

Ref	Expression
ffvelcdmd	|- ( ph -> ( F ` C ) e. B )

Proof of Theorem ffvelcdmd

Step	Hyp	Ref	Expression
1		ffvelcdmd.2	. 2 |- ( ph -> C e. A )
2		ffvelcdmd.1	. . 3 |- ( ph -> F : A --> B )
3	2	ffvelcdmda 5697	. 2 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )
4	1, 3	mpdan 421	1 |- ( ph -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   e. wcel 2167   -->wf 5254   ` cfv 5258

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-sbc 2990  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-opab 4095  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-fv 5266

This theorem is referenced by:  isotr  5863  caofinvl  6160  rdgon  6444  frecabcl  6457  phplem4dom  6923  fidceq  6930  dif1en  6940  fin0  6946  fin0or  6947  infm  6965  en2eqpr  6968  fidcenumlemrks  7019  fidcenumlemr  7021  supisoti  7076  ordiso2  7101  updjudhcoinlf  7146  updjudhcoinrg  7147  caseinl  7157  caseinr  7158  difinfsnlem  7165  difinfsn  7166  ctmlemr  7174  ctssdclemn0  7176  ctssdc  7179  enumctlemm  7180  enumct  7181  nnnninfeq2  7195  nninfisol  7199  enomnilem  7204  finomni  7206  ismkvnex  7221  enmkvlem  7227  enwomnilem  7235  nninfwlpoimlemg  7241  nninfwlpoimlemginf  7242  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  cauappcvgprlemm  7712  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdfu  7721  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlem2  7727  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgprlem2  7747  caucvgprprlemnkltj  7756  caucvgprprlemnkeqj  7757  caucvgprprlemnbj  7760  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  caucvgprprlemexb  7774  caucvgprprlemaddq  7775  caucvgprprlem1  7776  caucvgprprlem2  7777  caucvgsrlemcau  7860  caucvgsrlemgt1  7862  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  caucvgsr  7869  axcaucvglemval  7964  axcaucvglemcau  7965  axcaucvglemres  7966  fseq1p1m1  10169  4fvwrd4  10215  fvinim0ffz  10317  frecuzrdgg  10508  frecuzrdgsuctlem  10515  seq3val  10552  seqvalcd  10553  seq3p1  10557  seqp1cd  10562  ser3mono  10579  seq3split  10580  seq3caopr2  10585  iseqf1olemkle  10589  iseqf1olemklt  10590  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemmo  10597  iseqf1olemqk  10599  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seq3f1olemstep  10606  seq3f1oleml  10608  seq3f1o  10609  seqf1oglem2a  10610  seqf1oglem1  10611  seqf1oglem2  10612  seq3z  10620  seq3distr  10624  ser3ge0  10628  ser3le  10629  exp3vallem  10632  exp3val  10633  bcval5  10855  hashfz1  10875  resunimafz0  10923  leisorel  10929  zfz1isolemiso  10931  seq3coll  10934  caucvgrelemcau  11145  caucvgre  11146  cvg1nlemf  11148  cvg1nlemcau  11149  cvg1nlemres  11150  recvguniqlem  11159  resqrexlemdecn  11177  resqrexlemcalc3  11181  resqrexlemnmsq  11182  resqrexlemnm  11183  resqrexlemcvg  11184  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemga  11188  clim2ser  11502  clim2ser2  11503  climrecvg1n  11513  climcvg1nlem  11514  serf0  11517  sumeq2  11524  fsum3cvg  11543  summodclem2a  11546  fsum3  11552  fisumss  11557  fsumcl2lem  11563  fsumadd  11571  fsummulc2  11613  fsumrelem  11636  isumshft  11655  cvgratnnlemseq  11691  cvgratnnlemrate  11695  clim2prod  11704  clim2divap  11705  prodfrecap  11711  prodfdivap  11712  ntrivcvgap  11713  prodeq2  11722  fproddccvg  11737  prodmodclem3  11740  prodmodclem2a  11741  fprodseq  11748  fprodssdc  11755  fprodmul  11756  effsumlt  11857  nninfctlemfo  12207  nn0seqcvgd  12209  ialgrlem1st  12210  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  pcmpt2  12513  pcmptdvds  12514  1arithlem4  12535  1arith  12536  ennnfonelemdc  12616  ennnfonelemjn  12619  ennnfonelemg  12620  ennnfonelemp1  12623  ennnfonelemom  12625  ennnfonelemhdmp1  12626  ennnfonelemss  12627  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemnn0  12639  ennnfonelemim  12641  ctinfomlemom  12644  ctiunctlemudc  12654  ctiunctlemf  12655  ctiunctlemfo  12656  ssnnctlemct  12663  nninfdclemp1  12667  nninfdclemlt  12668  mhmf1o  13102  mhmco  13122  gsumfzcl  13131  isgrpinv  13186  imasgrp2  13240  mhmid  13245  mhmmnd  13246  ghmgrp  13248  mulgval  13252  mulgfng  13254  mulgnnsubcl  13264  ghmid  13379  ghminv  13380  ghmmulg  13386  ghmnsgpreima  13399  ghmeqker  13401  ghmf1  13403  kerf1ghm  13404  ghmf1o  13405  imasring  13620  rhmopp  13732  lspcl  13947  znidomb  14214  znrrg  14216  psrbaglesuppg  14226  iscnp4  14454  cnptopco  14458  lmtopcnp  14486  upxp  14508  uptx  14510  txlm  14515  comet  14735  metcnp3  14747  metcnp  14748  metcnp2  14749  metcnpi3  14753  elcncf2  14810  cncfco  14827  ivthreinc  14881  limcimolemlt  14900  cnplimcim  14903  cnplimclemle  14904  cnplimclemr  14905  limccnpcntop  14911  dvlemap  14916  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvef  14963  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993  plycolemc  14994  plycjlemc  14996  plycj  14997  plycn  14998  plyrecj  14999  dvply1  15001  dvply2g  15002  lgsval  15245  lgscllem  15248  lgsval2lem  15251  lgsval4a  15263  lgsneg  15265  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgseisenlem3  15313  lgseisenlem4  15314  1dom1el  15637  pwle2  15643  subctctexmid  15645  nnsf  15649  peano4nninf  15650  nninfalllem1  15652  nninfsellemdc  15654  nninfsellemeq  15658  nninfsellemqall  15659  nninfsellemeqinf  15660  nninfomnilem  15662  isomninnlem  15674  trilpolemeq1  15684  trilpolemlt1  15685  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696  nconstwlpolemgt0  15708  nconstwlpolem  15709