Theorem ffvelcdmd 5665

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 5664	. 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 2158   -->wf 5224   ` cfv 5228

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-v 2751  df-sbc 2975  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-opab 4077  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-fv 5236

This theorem is referenced by:  isotr  5830  caofinvl  6118  rdgon  6400  frecabcl  6413  phplem4dom  6875  fidceq  6882  dif1en  6892  fin0  6898  fin0or  6899  infm  6917  en2eqpr  6920  fidcenumlemrks  6965  fidcenumlemr  6967  supisoti  7022  ordiso2  7047  updjudhcoinlf  7092  updjudhcoinrg  7093  caseinl  7103  caseinr  7104  difinfsnlem  7111  difinfsn  7112  ctmlemr  7120  ctssdclemn0  7122  ctssdc  7125  enumctlemm  7126  enumct  7127  nnnninfeq2  7140  nninfisol  7144  enomnilem  7149  finomni  7151  ismkvnex  7166  enmkvlem  7172  enwomnilem  7180  nninfwlpoimlemg  7186  nninfwlpoimlemginf  7187  exmidfodomrlemr  7214  exmidfodomrlemrALT  7215  cauappcvgprlemm  7657  cauappcvgprlemdisj  7663  cauappcvgprlemloc  7664  cauappcvgprlemladdfu  7666  cauappcvgprlemladdru  7668  cauappcvgprlemladdrl  7669  cauappcvgprlem1  7671  cauappcvgprlem2  7672  caucvgprlemnkj  7678  caucvgprlemnbj  7679  caucvgprlemm  7680  caucvgprlemloc  7687  caucvgprlemladdfu  7689  caucvgprlemladdrl  7690  caucvgprlem1  7691  caucvgprlem2  7692  caucvgprprlemnkltj  7701  caucvgprprlemnkeqj  7702  caucvgprprlemnbj  7705  caucvgprprlemmu  7707  caucvgprprlemopl  7709  caucvgprprlemloc  7715  caucvgprprlemexbt  7718  caucvgprprlemexb  7719  caucvgprprlemaddq  7720  caucvgprprlem1  7721  caucvgprprlem2  7722  caucvgsrlemcau  7805  caucvgsrlemgt1  7807  caucvgsrlemoffcau  7810  caucvgsrlemoffres  7812  caucvgsr  7814  axcaucvglemval  7909  axcaucvglemcau  7910  axcaucvglemres  7911  fseq1p1m1  10107  4fvwrd4  10153  fvinim0ffz  10254  frecuzrdgg  10429  frecuzrdgsuctlem  10436  seq3val  10471  seqvalcd  10472  seq3p1  10475  seqp1cd  10479  ser3mono  10491  seq3split  10492  seq3caopr2  10495  iseqf1olemkle  10497  iseqf1olemklt  10498  iseqf1olemqcl  10499  iseqf1olemnab  10501  iseqf1olemmo  10505  iseqf1olemqk  10507  iseqf1olemjpcl  10508  iseqf1olemqpcl  10509  iseqf1olemfvp  10510  seq3f1olemqsumkj  10511  seq3f1olemqsumk  10512  seq3f1olemqsum  10513  seq3f1olemstep  10514  seq3f1oleml  10516  seq3f1o  10517  seq3z  10524  seq3distr  10526  ser3ge0  10530  ser3le  10531  exp3vallem  10534  exp3val  10535  bcval5  10756  hashfz1  10776  resunimafz0  10824  leisorel  10830  zfz1isolemiso  10832  seq3coll  10835  caucvgrelemcau  11002  caucvgre  11003  cvg1nlemf  11005  cvg1nlemcau  11006  cvg1nlemres  11007  recvguniqlem  11016  resqrexlemdecn  11034  resqrexlemcalc3  11038  resqrexlemnmsq  11039  resqrexlemnm  11040  resqrexlemcvg  11041  resqrexlemoverl  11043  resqrexlemglsq  11044  resqrexlemga  11045  clim2ser  11358  clim2ser2  11359  climrecvg1n  11369  climcvg1nlem  11370  serf0  11373  sumeq2  11380  fsum3cvg  11399  summodclem2a  11402  fsum3  11408  fisumss  11413  fsumcl2lem  11419  fsumadd  11427  fsummulc2  11469  fsumrelem  11492  isumshft  11511  cvgratnnlemseq  11547  cvgratnnlemrate  11551  clim2prod  11560  clim2divap  11561  prodfrecap  11567  prodfdivap  11568  ntrivcvgap  11569  prodeq2  11578  fproddccvg  11593  prodmodclem3  11596  prodmodclem2a  11597  fprodseq  11604  fprodssdc  11611  fprodmul  11612  effsumlt  11713  nn0seqcvgd  12054  ialgrlem1st  12055  eulerthlemrprm  12242  eulerthlema  12243  eulerthlemh  12244  pcmpt2  12355  pcmptdvds  12356  1arithlem4  12377  1arith  12378  ennnfonelemdc  12413  ennnfonelemjn  12416  ennnfonelemg  12417  ennnfonelemp1  12420  ennnfonelemom  12422  ennnfonelemhdmp1  12423  ennnfonelemss  12424  ennnfonelemkh  12426  ennnfonelemhf1o  12427  ennnfonelemex  12428  ennnfonelemhom  12429  ennnfonelemnn0  12436  ennnfonelemim  12438  ctinfomlemom  12441  ctiunctlemudc  12451  ctiunctlemf  12452  ctiunctlemfo  12453  ssnnctlemct  12460  nninfdclemp1  12464  nninfdclemlt  12465  mhmf1o  12880  mhmco  12893  isgrpinv  12948  imasgrp2  13002  mhmid  13007  mhmmnd  13008  ghmgrp  13010  mulgval  13014  mulgfng  13016  mulgnnsubcl  13024  imasring  13297  lspcl  13544  iscnp4  13958  cnptopco  13962  lmtopcnp  13990  upxp  14012  uptx  14014  txlm  14019  comet  14239  metcnp3  14251  metcnp  14252  metcnp2  14253  metcnpi3  14257  elcncf2  14301  cncfco  14318  limcimolemlt  14373  cnplimcim  14376  cnplimclemle  14377  cnplimclemr  14378  limccnpcntop  14384  dvlemap  14389  dvcnp2cntop  14403  dvaddxxbr  14405  dvmulxxbr  14406  dvcoapbr  14411  dvcjbr  14412  dvef  14428  lgsval  14645  lgscllem  14648  lgsval2lem  14651  lgsval4a  14663  lgsneg  14665  lgsdir  14676  lgsdilem2  14677  lgsdi  14678  lgsne0  14679  1dom1el  14983  pwle2  14989  subctctexmid  14991  nnsf  14995  peano4nninf  14996  nninfalllem1  14998  nninfsellemdc  15000  nninfsellemeq  15004  nninfsellemqall  15005  nninfsellemeqinf  15006  nninfomnilem  15008  isomninnlem  15019  trilpolemeq1  15029  trilpolemlt1  15030  iswomninnlem  15038  iswomni0  15040  ismkvnnlem  15041  nconstwlpolemgt0  15053  nconstwlpolem  15054