MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffvelrnd Structured version   Unicode version

Theorem ffvelrnd 6009
Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
ffvelrnd.1  |-  ( ph  ->  F : A --> B )
ffvelrnd.2  |-  ( ph  ->  C  e.  A )
Assertion
Ref Expression
ffvelrnd  |-  ( ph  ->  ( F `  C
)  e.  B )

Proof of Theorem ffvelrnd
StepHypRef Expression
1 ffvelrnd.2 . 2  |-  ( ph  ->  C  e.  A )
2 ffvelrnd.1 . . 3  |-  ( ph  ->  F : A --> B )
32ffvelrnda 6008 . 2  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
41, 3mpdan 666 1  |-  ( ph  ->  ( F `  C
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   -->wf 5564   ` cfv 5568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-fv 5576
This theorem is referenced by:  fpr2g  6111  f1dom3el3dif  6156  nvocnv  6167  fveqf1o  6187  soisores  6205  soisoi  6206  isotr  6214  weniso  6232  caofinvl  6548  ralxpmap  7505  enfixsn  7663  domunfican  7826  mapfienlem2  7898  supiso  7966  ordtypelem7  7982  wemaplem2  8005  cantnfle  8121  cantnflt  8122  cantnfp1lem3  8130  cantnfp1  8131  oemapvali  8134  cantnflem1b  8136  cantnflem1d  8138  cantnflem1  8139  cantnflem3  8141  cantnfleOLD  8151  cantnfltOLD  8152  cantnfp1lem3OLD  8156  cantnfp1OLD  8157  cantnflem1bOLD  8159  cantnflem1dOLD  8161  cantnflem1OLD  8162  cantnflem3OLD  8163  wemapwe  8170  wemapweOLD  8171  cnfcomlem  8174  cnfcom  8175  cnfcom2lem  8176  cnfcom2  8177  cnfcom3lem  8178  cnfcom3  8179  cnfcomlemOLD  8182  cnfcomOLD  8183  cnfcom2lemOLD  8184  cnfcom2OLD  8185  cnfcom3lemOLD  8186  cnfcom3OLD  8187  fseqenlem1  8436  fseqenlem2  8437  acndom  8463  acndom2  8466  iunfictbso  8526  dfac12lem2  8555  cofsmo  8680  infpssrlem4  8717  fin23lem30  8753  isf32lem8  8771  ttukeylem7  8926  iundom2g  8946  fpwwe2lem6  9042  fpwwe2lem7  9043  fpwwe2lem9  9045  canth4  9054  canthwelem  9057  pwfseqlem1  9065  pwfseqlem3  9067  pwfseqlem5  9070  fseq1p1m1  11805  4fvwrd4  11846  seqf1olem2a  12187  seqf1olem1  12188  seqf1olem2  12189  bcval5  12438  hashnn0pnf  12460  seqcoll  12559  seqcoll2  12560  ccatcl  12645  swrdcl  12698  revcl  12789  revlen  12790  ccatco  12855  rlimcn1  13558  o1rlimmul  13588  clim2ser  13624  clim2ser2  13625  isercolllem1  13634  isercolllem2  13635  isercoll  13637  isercoll2  13638  caucvgrlem  13642  caucvgrlem2  13644  serf0  13650  iseraltlem1  13651  iseraltlem2  13652  iseraltlem3  13653  sumrblem  13680  fsumcvg  13681  summolem2a  13684  fsumss  13694  fsummulc2  13748  cvgcmp  13779  cvgcmpce  13781  climcnds  13812  clim2prod  13847  clim2div  13848  prodrblem  13886  fprodcvg  13887  prodmolem2a  13891  fprodss  13905  effsumlt  14053  rpnnen2lem6  14160  ruclem9  14178  ruclem10  14179  sadcp1  14312  smupp1  14337  smuval2  14339  smupvallem  14340  nn0seqcvgd  14406  eulerthlem2  14519  pcmpt2  14619  pcmptdvds  14620  1arithlem4  14651  1arith  14652  vdwmc2  14704  vdwlem1  14706  vdwlem4  14709  vdwlem9  14714  vdwlem10  14715  0ram  14745  ramub1lem1  14751  ramub1lem2  14752  mrccl  15223  invisoinvl  15401  invcoisoid  15403  isocoinvid  15404  rcaninv  15405  funcsect  15483  funcinv  15484  funciso  15485  funcoppc  15486  cofucl  15499  cofuass  15500  funcres2b  15508  funcpropd  15511  funcres2c  15512  fullpropd  15531  fthsect  15536  fthinv  15537  fthmon  15538  ffthiso  15540  cofull  15545  cofth  15546  fuccocl  15575  fucidcl  15576  invfuc  15585  initoeu2lem1  15615  catcisolem  15707  catciso  15708  prfcl  15794  evlfcllem  15812  evlfcl  15813  uncf1  15827  uncf2  15828  curfuncf  15829  diag1cl  15833  diag2cl  15837  hofcl  15850  yon1cl  15854  oyon1cl  15862  yonedalem3a  15865  yonedalem4c  15868  yonedalem3b  15870  yonedainv  15872  yonffthlem  15873  gsumpropd2lem  16222  imasmnd2  16279  mhmf1o  16298  mhmco  16315  prdspjmhm  16320  frmdup2  16355  isgrpinv  16422  imasgrp2  16507  mhmid  16513  mhmmnd  16514  ghmgrp  16516  ghmid  16595  ghminv  16596  ghmmulg  16601  ghmnsgpreima  16613  ghmeqker  16615  ghmf1  16617  ghmf1o  16618  galactghm  16750  lactghmga  16751  f1omvdmvd  16790  psgnunilem5  16841  psgnunilem2  16842  psgnunilem3  16843  pj1id  17039  pj1eq  17040  efgsf  17069  efgsrel  17074  efgs1b  17076  efgredlemf  17081  efgredlemd  17084  efgredlemc  17085  efgredlem  17087  frgpup2  17116  frgpnabllem2  17200  frgpnabl  17201  ghmcyg  17220  gsumpt  17307  gsumptOLD  17308  gsummptfzcl  17315  dprdfadd  17378  dprdfeq0  17380  dprdfaddOLD  17385  dprdfeq0OLD  17387  dprdss  17394  dprdf1o  17397  subgdmdprd  17399  dprd2da  17409  dpjlem  17418  dpjf  17424  dpjidcl  17425  dpjlid  17428  dpjghm  17430  dpjghm2  17431  dpjidclOLD  17432  ablfac1b  17439  imasring  17586  isabvd  17787  islmhm2  18002  lmhmplusg  18008  lmhmvsca  18009  lmhmpropd  18037  pj1lmhm  18064  fidomndrnglem  18273  psrmulcllem  18358  psrlidm  18374  psrlidmOLD  18375  psrridm  18376  psrridmOLD  18377  psrass1  18378  psrdi  18379  psrdir  18380  psrass23l  18381  psrcom  18382  psrass23  18383  resspsrmul  18390  mvrcl2  18400  mplsubrglem  18418  mplsubrglemOLD  18419  mplmonmul  18444  mplcoe1  18445  mplcoe5  18449  mplcoe2OLD  18451  subrgasclcl  18482  evlslem2  18498  evlslem6  18499  evlslem6OLD  18500  evlslem3  18501  evlslem1  18502  evlsval2  18507  mpfconst  18517  mpfind  18523  psropprmul  18597  coe1mul2  18628  coe1tmmul2  18635  coe1pwmul  18638  cply1coe0bi  18660  coe1fzgsumdlem  18661  lply1binomsc  18667  evls1val  18675  evls1sca  18678  fveval1fvcl  18687  evl1scad  18689  evl1addd  18695  evl1subd  18696  evl1muld  18697  evl1expd  18699  evl1scvarpw  18717  domnchr  18867  znidomb  18896  znrrg  18900  frgpcyg  18908  psgnodpm  18920  regsumsupp  18954  frlmssuvc1  19119  frlmssuvc2  19120  frlmsslsp  19121  frlmup2  19124  lindfind2  19143  f1lindf  19147  mavmulcl  19339  mdetdiaglem  19390  mdetrlin  19394  mdetrsca  19395  mdetr0  19397  mdetero  19402  mdetunilem6  19409  mdetunilem7  19410  mdetunilem8  19411  mdetunilem9  19412  mdetuni0  19413  mdetmul  19415  maduf  19433  madutpos  19434  madugsum  19435  madurid  19436  madulid  19437  matinv  19469  matunit  19470  cramerimp  19478  mat2pmatbas  19517  m2cpmfo  19547  pmatcollpw3fi1lem1  19577  mply1topmatcl  19596  chpscmat  19633  chpscmatgsumbin  19635  chfacfisf  19645  chfacfisfcpmat  19646  chfacfscmulcl  19648  chfacfscmulgsum  19651  chfacfpmmulcl  19652  chfacfpmmulgsum  19655  chfacfpmmulgsum2  19656  cayhamlem1  19657  cpmadugsumlemF  19667  cpmadugsumfi  19668  cayhamlem4  19679  iscnp4  20055  cnprest2  20082  lmcnp  20096  cnt0  20138  cnhaus  20146  ptpjopn  20403  ptcnplem  20412  pthaus  20429  xkohaus  20444  pt1hmeo  20597  ptcmpfi  20604  xkohmeo  20606  cnpflfi  20790  tmdgsum  20884  symgtgp  20890  ghmcnp  20903  imasdsf1olem  21166  imasf1obl  21281  comet  21306  metcnp3  21333  metcnp  21334  metcnp2  21335  metcnpi3  21339  metustexhalfOLD  21356  metustexhalf  21357  metucnOLD  21381  metucn  21382  nrmmetd  21385  nmoi2  21527  nmoco  21534  nmotri  21536  nmods  21541  nghmcn  21542  metds0  21644  metdstri  21645  metdsre  21647  metdscnlem  21649  metdscn  21650  metnrmlem1a  21652  metnrmlem1  21653  elcncf2  21684  cncfco  21701  cnheibor  21745  lebnumlem1  21751  lebnumlem3  21753  pi1cof  21849  pi1coghm  21851  nmoleub2lem  21887  nmoleub2lem3  21888  nmoleub3  21892  lmnn  21992  iscauf  22009  caucfil  22012  equivcau  22029  caubl  22036  caublcls  22037  lmcau  22041  rrxdstprj1  22126  pmltpclem2  22151  evthicc2  22162  ovoliunlem1  22203  ovoliunlem2  22204  ovolicc2lem1  22218  ovolicc2lem2  22219  ovolicc2lem3  22220  ovolicc2lem4  22221  volsup  22256  uniioombllem3  22284  volcn  22305  vitalilem2  22308  vitalilem3  22309  i1faddlem  22390  i1fmullem  22391  mbfi1fseqlem6  22417  mbfmullem2  22421  itg2monolem1  22447  limccnp  22585  dvlem  22590  dvcnp2  22613  dvaddbr  22631  dvmulbr  22632  dvcmul  22637  dvcobr  22639  dvcjbr  22642  dvcnvlem  22667  dvef  22671  dvferm1lem  22675  dvferm1  22676  dvferm2lem  22677  dvferm2  22678  dvferm  22679  rolle  22681  cmvth  22682  mvth  22683  dvlip  22684  dvlipcn  22685  c1liplem1  22687  dveq0  22691  dv11cn  22692  dvgt0  22695  dvlt0  22696  dvge0  22697  dvivthlem1  22699  dvivth  22701  lhop1lem  22704  lhop2  22706  dvcnvrelem1  22708  dvcnvrelem2  22709  dvcvx  22711  dvfsumlem3  22719  dvfsumrlim  22722  dvfsumrlim2  22723  ftc1a  22728  ftc1lem4  22730  ftc1lem5  22731  ftc1lem6  22732  ftc2  22735  ftc2ditg  22737  itgsubst  22740  tdeglem4  22748  mdegle0  22767  mdegmullem  22768  deg1ldgdomn  22784  deg1add  22794  deg1sublt  22801  deg1mul2  22805  deg1mul3  22806  deg1mul3le  22807  ply1nz  22812  ply1divex  22827  uc1pmon1p  22842  ply1remlem  22853  ply1rem  22854  fta1glem1  22856  fta1glem2  22857  fta1g  22858  fta1blem  22859  drnguc1p  22861  ig1peu  22862  plyeq0lem  22897  dgrub  22921  coemullem  22937  coemulhi  22941  dgradd2  22955  dgrmul  22957  dgrcolem2  22961  plymul0or  22967  dvply1  22970  dvply2g  22971  plydivlem4  22982  vieta1lem2  22997  plyexmo  22999  elqaalem2  23006  elqaalem3  23007  aareccl  23012  aalioulem3  23020  aalioulem4  23021  taylfvallem1  23042  tayl0  23047  taylply2  23053  taylply  23054  dvtaylp  23055  taylthlem1  23058  taylthlem2  23059  ulmclm  23072  ulmshftlem  23074  ulmshft  23075  ulmcaulem  23079  ulmcau  23080  ulmbdd  23083  ulmcn  23084  ulmdvlem1  23085  mtest  23089  mtestbdd  23090  radcnvlem1  23098  pserulm  23107  psercn  23111  pserdvlem2  23113  abelthlem5  23120  abelthlem7  23123  abelthlem9  23125  abelth  23126  eff1olem  23225  efabl  23227  efsubm  23228  efrlim  23623  scvxcvx  23639  jensenlem1  23640  jensenlem2  23641  jensen  23642  amgm  23644  ftalem1  23725  ftalem2  23726  ftalem3  23727  ftalem4  23728  ftalem5  23729  ftalem7  23731  dchrelbas3  23892  dchrzrhcl  23899  dchrzrhmul  23900  dchrn0  23904  dchrinvcl  23907  dchrabs  23914  dchrinv  23915  dchrptlem1  23918  dchrptlem2  23919  dchrsum2  23922  sumdchr2  23924  dchrhash  23925  sum2dchr  23928  bposlem3  23940  bposlem5  23942  bposlem6  23943  lgsval2lem  23960  lgsqrlem1  23995  lgsqrlem2  23996  lgsqrlem3  23997  lgsqrlem4  23998  lgseisenlem3  24005  lgseisenlem4  24006  rpvmasumlem  24051  dchrisumlem3  24055  dchrmusum2  24058  dchrvmasumlem3  24063  dchrvmasumiflem1  24065  dchrisum0ff  24071  dchrisum0flblem1  24072  dchrisum0flblem2  24073  rpvmasum2  24076  dchrisum0re  24077  dchrisum0lem1b  24079  motcl  24307  motco  24308  cnvmot  24309  motcgrg  24312  mircl  24425  mirbtwni  24434  mirbtwnb  24435  mirauto  24444  miduniq2  24447  krippenlem  24450  lmicl  24535  f1otrg  24578  f1otrge  24579  axcontlem10  24680  wlkonwlk  24941  nvnencycllem  25047  wlkiswwlk1  25094  clwlkisclwwlklem1  25191  eupap1  25380  eupath2lem3  25383  eupath2  25384  vdgfrgragt2  25431  ghomidOLD  25767  ghgrpOLD  25770  lno0  26071  lnomul  26075  ubthlem2  26187  ubthlem3  26188  minvecolem3  26192  chscllem2  26956  chscllem3  26957  off2  27910  aciunf1lem  27932  abliso  28124  gsumle  28207  rhmdvd  28250  kerunit  28252  qtophaus  28278  reff  28281  tpr2rico  28333  lmdvg  28374  pl1cn  28376  qqhval2lem  28400  qqhf  28405  qqhghm  28407  qqhrhm  28408  qqhnm  28409  qqhcn  28410  qqhre  28436  esumfzf  28502  esumfsup  28503  esumpcvgval  28511  esumcocn  28513  esumcvg  28519  sigapildsys  28596  volmeas  28666  omscl  28729  oms0  28731  omsmon  28732  omssubaddlem  28733  omssubadd  28734  baselcarsg  28740  difelcarsg  28744  inelcarsg  28745  carsgsigalem  28749  carsgclctunlem1  28751  carsggect  28752  carsgclctunlem2  28753  carsgclctunlem3  28754  carsgclctun  28755  omsmeas  28757  pmeasmono  28758  pmeasadd  28759  eulerpartlemsv2  28789  eulerpartlemsf  28790  eulerpartlemsv3  28792  eulerpartlemv  28795  eulerpartlemf  28801  eulerpartlemgh  28809  eulerpartlemgs2  28811  sseqf  28823  sseqp1  28826  fiblem  28829  dstfrvel  28904  plymulx0  28996  plyrecld  28998  signsplypnf  28999  signsply0  29000  signstcl  29014  signstf  29015  signstfvn  29018  signsvtn0  29019  signsvtp  29032  signsvtn  29033  signsvfpn  29034  signsvfnn  29035  signlem0  29036  subfacp1lem5  29468  erdszelem7  29481  erdszelem8  29482  erdszelem9  29483  cvxscon  29527  cvmopnlem  29562  cvmfolem  29563  cvmliftmolem1  29565  cvmliftmolem2  29566  cvmliftlem1  29569  cvmliftlem6  29574  cvmliftlem7  29575  cvmlift2lem5  29591  cvmlift2lem7  29593  cvmlift2lem10  29596  cvmlift3lem6  29608  cvmlift3lem7  29609  cvmlift3lem9  29611  mrsubcv  29709  elmrsubrn  29719  mrsubco  29720  mrsubvrs  29721  msubco  29730  msubff1  29755  msubvrs  29759  mclsind  29769  mclsppslem  29782  sinccvglem  29877  iprodefisumlem  29936  fwddifn0  30489  fwddifnp1  30490  heicant  31401  ftc1cnnclem  31441  ftc1cnnc  31442  ftc2nc  31452  f1ocan1fv  31479  sdclem2  31497  caushft  31516  heibor1lem  31567  bfplem1  31580  bfplem2  31581  rrndstprj1  31588  rrncmslem  31590  lflcl  32062  tendocl  33766  lcfrlem13  34555  mapdcl  34653  hvmapclN  34764  hvmapcl2  34766  ismrcd1  34972  mzpindd  35020  diophin  35047  diophun  35048  mzpcong  35251  fnwe2lem3  35340  hbtlem2  35417  dgrsub2  35428  mpaaeu  35443  cnsrplycl  35460  idomrootle  35496  imo72b2lem0  35973  imo72b2  35984  fmuldfeqlem1  36925  fmuldfeq  36926  mccllem  36954  sumnnodd  36985  cncfshift  37025  cncfcompt  37034  icccncfext  37039  cncfiooiccre  37047  cncfioobdlem  37048  fperdvper  37064  dvbdfbdioolem1  37074  dvbdfbdioolem2  37075  dvbdfbdioo  37076  ioodvbdlimc1lem1  37077  ioodvbdlimc1lem2  37078  ioodvbdlimc2lem  37080  dvnmul  37089  dvnprodlem1  37092  dvnprodlem2  37093  itgsubsticc  37124  itgioocnicc  37125  itgspltprt  37127  itgiccshift  37128  itgperiod  37129  itgsbtaddcnst  37130  stoweidlem3  37134  stoweidlem5  37136  stoweidlem11  37142  stoweidlem16  37147  stoweidlem17  37148  stoweidlem20  37151  stoweidlem22  37153  stoweidlem23  37154  stoweidlem24  37155  stoweidlem25  37156  stoweidlem26  37157  stoweidlem28  37159  stoweidlem32  37163  stoweidlem36  37167  stoweidlem42  37173  stoweidlem48  37179  stoweidlem51  37182  stoweidlem52  37183  stoweidlem59  37190  stirlinglem8  37212  stirlinglem15  37219  dirkercncflem2  37235  fourierdlem1  37239  fourierdlem9  37247  fourierdlem11  37249  fourierdlem12  37250  fourierdlem13  37251  fourierdlem14  37252  fourierdlem15  37253  fourierdlem16  37254  fourierdlem19  37257  fourierdlem20  37258  fourierdlem21  37259  fourierdlem22  37260  fourierdlem25  37263  fourierdlem27  37265  fourierdlem28  37266  fourierdlem39  37277  fourierdlem40  37278  fourierdlem41  37279  fourierdlem42  37280  fourierdlem46  37284  fourierdlem48  37286  fourierdlem49  37287  fourierdlem50  37288  fourierdlem52  37290  fourierdlem54  37292  fourierdlem57  37295  fourierdlem59  37297  fourierdlem60  37298  fourierdlem61  37299  fourierdlem63  37301  fourierdlem64  37302  fourierdlem65  37303  fourierdlem66  37304  fourierdlem68  37306  fourierdlem69  37307  fourierdlem70  37308  fourierdlem71  37309  fourierdlem72  37310  fourierdlem73  37311  fourierdlem74  37312  fourierdlem75  37313  fourierdlem76  37314  fourierdlem78  37316  fourierdlem79  37317  fourierdlem80  37318  fourierdlem81  37319  fourierdlem83  37321  fourierdlem84  37322  fourierdlem85  37323  fourierdlem87  37325  fourierdlem88  37326  fourierdlem89  37327  fourierdlem90  37328  fourierdlem91  37329  fourierdlem92  37330  fourierdlem93  37331  fourierdlem94  37332  fourierdlem95  37333  fourierdlem97  37335  fourierdlem101  37339  fourierdlem102  37340  fourierdlem103  37341  fourierdlem104  37342  fourierdlem107  37345  fourierdlem111  37349  fourierdlem112  37350  fourierdlem113  37351  fourierdlem114  37352  fouriercnp  37358  sqwvfoura  37360  elaa2lem  37365  etransclem2  37368  etransclem3  37369  etransclem7  37373  etransclem10  37376  etransclem14  37380  etransclem15  37381  etransclem18  37384  etransclem23  37389  etransclem24  37390  etransclem25  37391  etransclem27  37393  etransclem31  37397  etransclem32  37398  etransclem33  37399  etransclem34  37400  etransclem35  37401  etransclem39  37405  etransclem44  37410  etransclem45  37411  etransclem46  37412  etransclem47  37413  etransclem48  37414  iccpartxr  37667  lswn0  37847  imarnf1pr  37923  mgmhmf1o  38085  mgmhmco  38099  linply1  38485  fdivmptf  38653  refdivmptf  38654
  Copyright terms: Public domain W3C validator