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

Theorem ffvelrnd 5839
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 5838 . 2  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
41, 3mpdan 668 1  |-  ( ph  ->  ( F `  C
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   -->wf 5409   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
This theorem is referenced by:  f1dom3el3dif  5976  nvocnv  5983  fveqf1o  5995  soisores  6013  soisoi  6014  isotr  6022  weniso  6040  caofinvl  6342  ralxpmap  7254  enfixsn  7412  domunfican  7576  mapfienlem2  7647  supiso  7714  ordtypelem7  7730  wemaplem2  7753  cantnfle  7871  cantnflt  7872  cantnfp1lem3  7880  cantnfp1  7881  oemapvali  7884  cantnflem1b  7886  cantnflem1d  7888  cantnflem1  7889  cantnflem3  7891  cantnfleOLD  7901  cantnfltOLD  7902  cantnfp1lem3OLD  7906  cantnfp1OLD  7907  cantnflem1bOLD  7909  cantnflem1dOLD  7911  cantnflem1OLD  7912  cantnflem3OLD  7913  wemapwe  7920  wemapweOLD  7921  cnfcomlem  7924  cnfcom  7925  cnfcom2lem  7926  cnfcom2  7927  cnfcom3lem  7928  cnfcom3  7929  cnfcomlemOLD  7932  cnfcomOLD  7933  cnfcom2lemOLD  7934  cnfcom2OLD  7935  cnfcom3lemOLD  7936  cnfcom3OLD  7937  fseqenlem1  8186  fseqenlem2  8187  acndom  8213  acndom2  8216  iunfictbso  8276  dfac12lem2  8305  cofsmo  8430  infpssrlem4  8467  fin23lem30  8503  isf32lem8  8521  ttukeylem7  8676  iundom2g  8696  fpwwe2lem6  8794  fpwwe2lem7  8795  fpwwe2lem9  8797  canth4  8806  canthwelem  8809  pwfseqlem1  8817  pwfseqlem3  8819  pwfseqlem5  8822  4fvwrd4  11525  fseq1p1m1  11526  seqf1olem2a  11836  seqf1olem1  11837  seqf1olem2  11838  bcval5  12086  hashnn0pnf  12105  seqcoll  12208  seqcoll2  12209  lswcl  12262  ccatcl  12266  swrdcl  12307  wrdind  12363  wrd2ind  12364  revcl  12393  revlen  12394  ccatco  12455  rlimcn1  13058  o1rlimmul  13088  clim2ser  13124  clim2ser2  13125  isercolllem1  13134  isercolllem2  13135  isercoll  13137  isercoll2  13138  caucvgrlem  13142  caucvgrlem2  13144  serf0  13150  iseraltlem1  13151  iseraltlem2  13152  iseraltlem3  13153  sumrblem  13180  fsumcvg  13181  summolem2a  13184  fsumss  13194  fsummulc2  13243  cvgcmp  13271  cvgcmpce  13273  climcnds  13306  effsumlt  13387  rpnnen2lem6  13494  ruclem9  13512  ruclem10  13513  sadcp1  13643  smupp1  13668  smuval2  13670  smupvallem  13671  nn0seqcvgd  13737  eulerthlem2  13849  pcmpt2  13947  pcmptdvds  13948  1arithlem4  13979  1arith  13980  vdwmc2  14032  vdwlem1  14034  vdwlem4  14037  vdwlem9  14042  vdwlem10  14043  0ram  14073  ramub1lem1  14079  ramub1lem2  14080  mrccl  14541  funcsect  14774  funcinv  14775  funciso  14776  funcoppc  14777  cofucl  14790  cofuass  14791  funcres2b  14799  funcpropd  14802  funcres2c  14803  fullpropd  14822  fthsect  14827  fthinv  14828  fthmon  14829  ffthiso  14831  cofull  14836  cofth  14837  fuccocl  14866  fucidcl  14867  invfuc  14876  catcisolem  14966  catciso  14967  prfcl  15005  evlfcllem  15023  evlfcl  15024  uncf1  15038  uncf2  15039  curfuncf  15040  diag1cl  15044  diag2cl  15048  hofcl  15061  yon1cl  15065  oyon1cl  15073  yonedalem3a  15076  yonedalem4c  15079  yonedalem3b  15081  yonedainv  15083  yonffthlem  15084  imasmnd2  15450  mhmco  15481  prdspjmhm  15486  gsumpropd2lem  15496  frmdup2  15534  isgrpinv  15579  imasgrp2  15661  ghmid  15744  ghminv  15745  ghmmulg  15750  ghmnsgpreima  15762  ghmeqker  15764  ghmf1  15766  ghmf1o  15767  galactghm  15899  lactghmga  15900  f1omvdmvd  15940  psgnunilem5  15991  psgnunilem2  15992  psgnunilem3  15993  pj1id  16187  pj1eq  16188  efgsf  16217  efgsrel  16222  efgs1b  16224  efgredlemf  16229  efgredlemd  16232  efgredlemc  16233  efgredlem  16235  frgpup2  16264  frgpnabllem2  16343  frgpnabl  16344  ghmcyg  16363  gsumpt  16443  gsumptOLD  16444  gsummptfzcl  16448  dprdfadd  16498  dprdfeq0  16500  dprdfaddOLD  16505  dprdfeq0OLD  16507  dprdss  16514  subgdmdprd  16519  dprd2da  16529  dpjlem  16538  dpjf  16544  dpjidcl  16545  dpjlid  16548  dpjghm  16550  dpjghm2  16551  dpjidclOLD  16552  ablfac1b  16559  imasrng  16699  isabvd  16883  islmhm2  17096  lmhmplusg  17102  lmhmvsca  17103  lmhmpropd  17131  pj1lmhm  17158  fidomndrnglem  17355  psrmulcllem  17435  psrlidm  17451  psrlidmOLD  17452  psrridm  17453  psrridmOLD  17454  psrass1  17455  psrdi  17456  psrdir  17457  psrcom  17458  psrass23  17459  resspsrmul  17466  mvrcl2  17476  mplsubrglem  17494  mplsubrglemOLD  17495  mplmonmul  17520  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  subrgasclcl  17556  evlslem2  17572  evlslem6  17573  evlslem6OLD  17574  evlslem3  17575  evlslem1  17576  evlsval2  17581  mpfconst  17591  mpfind  17597  psropprmul  17668  coe1mul2  17698  coe1tmmul2  17704  coe1pwmul  17707  evls1val  17730  evls1sca  17733  fveval1fvcl  17742  evl1scad  17744  evl1addd  17750  evl1subd  17751  evl1muld  17752  evl1expd  17754  evl1scvarpw  17772  domnchr  17938  znidomb  17969  znrrg  17973  frgpcyg  17981  psgnodpm  17993  regsumsupp  18027  frlmssuvc1  18194  frlmssuvc2  18195  frlmssuvc1OLD  18196  frlmssuvc2OLD  18197  frlmsslsp  18198  frlmsslspOLD  18199  frlmup2  18202  lindfind2  18222  f1lindf  18226  mavmulcl  18333  mdet1  18383  mdetrlin  18384  mdetrsca  18385  mdetr0  18387  mdetero  18391  mdetunilem6  18398  mdetunilem7  18399  mdetunilem8  18400  mdetunilem9  18401  mdetuni0  18402  mdetmul  18404  maduf  18422  madutpos  18423  madugsum  18424  madurid  18425  madulid  18426  matinv  18458  matunit  18459  cramerimp  18467  iscnp4  18842  cnprest2  18869  lmcnp  18883  cnt0  18925  cnhaus  18933  ptpjopn  19160  ptcnplem  19169  pthaus  19186  xkohaus  19201  pt1hmeo  19354  ptcmpfi  19361  xkohmeo  19363  cnpflfi  19547  tmdgsum  19641  symgtgp  19647  ghmcnp  19660  imasdsf1olem  19923  imasf1obl  20038  comet  20063  metcnp3  20090  metcnp  20091  metcnp2  20092  metcnpi3  20096  metustexhalfOLD  20113  metustexhalf  20114  metucnOLD  20138  metucn  20139  nrmmetd  20142  nmoi2  20284  nmoco  20291  nmotri  20293  nmods  20298  nghmcn  20299  metds0  20401  metdstri  20402  metdsre  20404  metdscnlem  20406  metdscn  20407  metnrmlem1a  20409  metnrmlem1  20410  elcncf2  20441  cncfco  20458  cnheibor  20502  lebnumlem1  20508  lebnumlem3  20510  pi1cof  20606  pi1coghm  20608  nmoleub2lem  20644  nmoleub2lem3  20645  nmoleub3  20649  lmnn  20749  iscauf  20766  caucfil  20769  equivcau  20786  caubl  20793  caublcls  20794  lmcau  20798  rrxdstprj1  20883  pmltpclem2  20908  evthicc2  20919  ovoliunlem1  20960  ovoliunlem2  20961  ovolicc2lem1  20975  ovolicc2lem2  20976  ovolicc2lem3  20977  ovolicc2lem4  20978  volsup  21012  uniioombllem3  21040  volcn  21061  vitalilem2  21064  vitalilem3  21065  i1faddlem  21146  i1fmullem  21147  mbfi1fseqlem6  21173  mbfmullem2  21177  itg2monolem1  21203  limccnp  21341  dvlem  21346  dvcnp2  21369  dvaddbr  21387  dvmulbr  21388  dvcmul  21393  dvcobr  21395  dvcjbr  21398  dvcnvlem  21423  dvef  21427  dvferm1lem  21431  dvferm1  21432  dvferm2lem  21433  dvferm2  21434  dvferm  21435  rolle  21437  cmvth  21438  mvth  21439  dvlip  21440  dvlipcn  21441  c1liplem1  21443  dveq0  21447  dv11cn  21448  dvgt0  21451  dvlt0  21452  dvge0  21453  dvivthlem1  21455  dvivth  21457  lhop1lem  21460  lhop2  21462  dvcnvrelem1  21464  dvcnvrelem2  21465  dvcvx  21467  dvfsumlem3  21475  dvfsumrlim  21478  dvfsumrlim2  21479  ftc1a  21484  ftc1lem4  21486  ftc1lem5  21487  ftc1lem6  21488  ftc2  21491  ftc2ditg  21493  itgsubst  21496  tdeglem4  21504  mdegle0  21523  mdegmullem  21524  deg1ldgdomn  21540  deg1add  21550  deg1sublt  21557  deg1mul2  21561  deg1mul3  21562  deg1mul3le  21563  ply1nz  21568  ply1divex  21583  uc1pmon1p  21598  ply1remlem  21609  ply1rem  21610  facth1  21611  fta1glem1  21612  fta1glem2  21613  fta1g  21614  fta1blem  21615  drnguc1p  21617  ig1peu  21618  plyeq0lem  21653  dgrub  21677  coemullem  21692  coemulhi  21696  dgradd2  21710  dgrmul  21712  dgrcolem2  21716  plymul0or  21722  dvply1  21725  dvply2g  21726  plydivlem4  21737  vieta1lem2  21752  plyexmo  21754  elqaalem2  21761  elqaalem3  21762  aareccl  21767  aalioulem3  21775  aalioulem4  21776  taylfvallem1  21797  tayl0  21802  taylply2  21808  taylply  21809  dvtaylp  21810  taylthlem1  21813  taylthlem2  21814  ulmclm  21827  ulmshftlem  21829  ulmshft  21830  ulmcaulem  21834  ulmcau  21835  ulmbdd  21838  ulmcn  21839  ulmdvlem1  21840  mtest  21844  mtestbdd  21845  radcnvlem1  21853  pserulm  21862  psercn  21866  pserdvlem2  21868  abelthlem5  21875  abelthlem7  21878  abelthlem9  21880  abelth  21881  eff1olem  21979  efrlim  22338  scvxcvx  22354  jensenlem1  22355  jensenlem2  22356  jensen  22357  amgm  22359  ftalem1  22385  ftalem2  22386  ftalem3  22387  ftalem4  22388  ftalem5  22389  ftalem7  22391  dchrelbas3  22552  dchrzrhcl  22559  dchrzrhmul  22560  dchrn0  22564  dchrinvcl  22567  dchrabs  22574  dchrinv  22575  dchrptlem1  22578  dchrptlem2  22579  dchrsum2  22582  sumdchr2  22584  dchrhash  22585  sum2dchr  22588  bposlem3  22600  bposlem5  22602  bposlem6  22603  lgsval2lem  22620  lgsqrlem1  22655  lgsqrlem2  22656  lgsqrlem3  22657  lgsqrlem4  22658  lgseisenlem3  22665  lgseisenlem4  22666  rpvmasumlem  22711  dchrisumlem3  22715  dchrmusum2  22718  dchrvmasumlem3  22723  dchrvmasumiflem1  22725  dchrisum0ff  22731  dchrisum0flblem1  22732  dchrisum0flblem2  22733  rpvmasum2  22736  dchrisum0re  22737  dchrisum0lem1b  22739  mirmir  23033  mirreu  23034  mireq  23035  miriso  23039  mirbtwni  23040  mirbtwnb  23041  mirauto  23043  miduniq  23044  miduniq1  23045  miduniq2  23046  krippenlem  23049  ragcom  23057  ragcol  23058  ragmir  23059  ragflat2  23061  ragflat  23062  ragcgr  23065  f1otrg  23068  f1otrge  23069  axcontlem10  23170  wlkonwlk  23385  nvnencycllem  23480  eupap1  23548  eupath2lem3  23551  eupath2  23552  ghomid  23803  ghgrp  23806  lno0  24107  lnomul  24111  ubthlem2  24223  ubthlem3  24224  minvecolem3  24228  chscllem2  24992  chscllem3  24993  off2  25910  abliso  26110  gsumle  26197  rhmdvd  26240  kerunit  26242  tpr2rico  26294  lmdvg  26335  pl1cn  26337  qqhval2lem  26362  qqhf  26367  qqhghm  26369  qqhrhm  26370  qqhnm  26371  qqhcn  26372  qqhre  26398  esumfzf  26470  esumfsup  26471  esumpcvgval  26479  esumcocn  26481  esumcvg  26487  volmeas  26599  oms0  26662  omsmon  26663  eulerpartlemsv2  26693  eulerpartlemsf  26694  eulerpartlemsv3  26696  eulerpartlemv  26699  eulerpartlemf  26705  eulerpartlemgh  26713  eulerpartlemgs2  26715  sseqf  26727  sseqp1  26730  fiblem  26733  dstfrvel  26808  plymulx0  26900  plyrecld  26902  signsplypnf  26903  signsply0  26904  signstcl  26918  signstf  26919  signstfvn  26922  signsvtn0  26923  signsvtp  26936  signsvtn  26937  signsvfpn  26938  signsvfnn  26939  signlem0  26940  subfacp1lem5  27024  erdszelem7  27037  erdszelem8  27038  erdszelem9  27039  cvxscon  27084  cvmopnlem  27119  cvmfolem  27120  cvmliftmolem1  27122  cvmliftmolem2  27123  cvmliftlem1  27126  cvmliftlem6  27131  cvmliftlem7  27132  cvmlift2lem5  27148  cvmlift2lem7  27150  cvmlift2lem10  27153  cvmlift3lem6  27165  cvmlift3lem7  27166  cvmlift3lem9  27168  sinccvglem  27268  clim2prod  27354  clim2div  27355  prodrblem  27393  fprodcvg  27394  prodmolem2a  27398  fprodss  27412  iprodefisumlem  27455  heicant  28379  ftc1cnnclem  28418  ftc1cnnc  28419  ftc2nc  28429  f1ocan1fv  28573  sdclem2  28591  caushft  28610  heibor1lem  28661  bfplem1  28674  bfplem2  28675  rrndstprj1  28682  rrncmslem  28684  ismrcd1  28987  mzpindd  29035  diophin  29064  diophun  29065  mzpcong  29268  fnwe2lem3  29358  hbtlem2  29433  dgrsub2  29444  mpaaeu  29460  cnsrplycl  29477  idomrootle  29513  fmuldfeqlem1  29716  fmuldfeq  29717  stoweidlem3  29751  stoweidlem5  29753  stoweidlem11  29759  stoweidlem16  29764  stoweidlem17  29765  stoweidlem20  29768  stoweidlem22  29770  stoweidlem23  29771  stoweidlem24  29772  stoweidlem25  29773  stoweidlem26  29774  stoweidlem28  29776  stoweidlem32  29780  stoweidlem36  29784  stoweidlem42  29790  stoweidlem48  29796  stoweidlem51  29799  stoweidlem52  29800  stoweidlem59  29807  stirlinglem8  29829  stirlinglem15  29836  imarnf1pr  30103  lswn0  30211  wlkiswwlk1  30277  clwlkisclwwlklem1  30402  vdgfrgragt2  30573  psrass23l  30763  lply1binomsc  30775  linply1  30776  pmatcollpw1lem2  30815  mdetdiaglem  30824  lflcl  32549  tendocl  34251  lcfrlem13  35040  mapdcl  35138  hvmapclN  35249  hvmapcl2  35251
  Copyright terms: Public domain W3C validator