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

Theorem ffvelrnd 5956
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 5955 . 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 1758   -->wf 5525   ` cfv 5529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-fv 5537
This theorem is referenced by:  f1dom3el3dif  6093  nvocnv  6100  fveqf1o  6112  soisores  6130  soisoi  6131  isotr  6139  weniso  6157  caofinvl  6460  ralxpmap  7375  enfixsn  7533  domunfican  7698  mapfienlem2  7769  supiso  7836  ordtypelem7  7852  wemaplem2  7875  cantnfle  7993  cantnflt  7994  cantnfp1lem3  8002  cantnfp1  8003  oemapvali  8006  cantnflem1b  8008  cantnflem1d  8010  cantnflem1  8011  cantnflem3  8013  cantnfleOLD  8023  cantnfltOLD  8024  cantnfp1lem3OLD  8028  cantnfp1OLD  8029  cantnflem1bOLD  8031  cantnflem1dOLD  8033  cantnflem1OLD  8034  cantnflem3OLD  8035  wemapwe  8042  wemapweOLD  8043  cnfcomlem  8046  cnfcom  8047  cnfcom2lem  8048  cnfcom2  8049  cnfcom3lem  8050  cnfcom3  8051  cnfcomlemOLD  8054  cnfcomOLD  8055  cnfcom2lemOLD  8056  cnfcom2OLD  8057  cnfcom3lemOLD  8058  cnfcom3OLD  8059  fseqenlem1  8308  fseqenlem2  8309  acndom  8335  acndom2  8338  iunfictbso  8398  dfac12lem2  8427  cofsmo  8552  infpssrlem4  8589  fin23lem30  8625  isf32lem8  8643  ttukeylem7  8798  iundom2g  8818  fpwwe2lem6  8916  fpwwe2lem7  8917  fpwwe2lem9  8919  canth4  8928  canthwelem  8931  pwfseqlem1  8939  pwfseqlem3  8941  pwfseqlem5  8944  4fvwrd4  11653  fseq1p1m1  11654  seqf1olem2a  11964  seqf1olem1  11965  seqf1olem2  11966  bcval5  12214  hashnn0pnf  12233  seqcoll  12337  seqcoll2  12338  lswcl  12391  ccatcl  12395  swrdcl  12436  wrdind  12492  wrd2ind  12493  revcl  12522  revlen  12523  ccatco  12584  rlimcn1  13187  o1rlimmul  13217  clim2ser  13253  clim2ser2  13254  isercolllem1  13263  isercolllem2  13264  isercoll  13266  isercoll2  13267  caucvgrlem  13271  caucvgrlem2  13273  serf0  13279  iseraltlem1  13280  iseraltlem2  13281  iseraltlem3  13282  sumrblem  13309  fsumcvg  13310  summolem2a  13313  fsumss  13323  fsummulc2  13372  cvgcmp  13400  cvgcmpce  13402  climcnds  13435  effsumlt  13516  rpnnen2lem6  13623  ruclem9  13641  ruclem10  13642  sadcp1  13772  smupp1  13797  smuval2  13799  smupvallem  13800  nn0seqcvgd  13866  eulerthlem2  13978  pcmpt2  14076  pcmptdvds  14077  1arithlem4  14108  1arith  14109  vdwmc2  14161  vdwlem1  14163  vdwlem4  14166  vdwlem9  14171  vdwlem10  14172  0ram  14202  ramub1lem1  14208  ramub1lem2  14209  mrccl  14671  funcsect  14904  funcinv  14905  funciso  14906  funcoppc  14907  cofucl  14920  cofuass  14921  funcres2b  14929  funcpropd  14932  funcres2c  14933  fullpropd  14952  fthsect  14957  fthinv  14958  fthmon  14959  ffthiso  14961  cofull  14966  cofth  14967  fuccocl  14996  fucidcl  14997  invfuc  15006  catcisolem  15096  catciso  15097  prfcl  15135  evlfcllem  15153  evlfcl  15154  uncf1  15168  uncf2  15169  curfuncf  15170  diag1cl  15174  diag2cl  15178  hofcl  15191  yon1cl  15195  oyon1cl  15203  yonedalem3a  15206  yonedalem4c  15209  yonedalem3b  15211  yonedainv  15213  yonffthlem  15214  imasmnd2  15580  mhmf1o  15595  mhmco  15612  prdspjmhm  15617  gsumpropd2lem  15627  frmdup2  15665  isgrpinv  15710  imasgrp2  15792  ghmid  15875  ghminv  15876  ghmmulg  15881  ghmnsgpreima  15893  ghmeqker  15895  ghmf1  15897  ghmf1o  15898  galactghm  16030  lactghmga  16031  f1omvdmvd  16071  psgnunilem5  16122  psgnunilem2  16123  psgnunilem3  16124  pj1id  16320  pj1eq  16321  efgsf  16350  efgsrel  16355  efgs1b  16357  efgredlemf  16362  efgredlemd  16365  efgredlemc  16366  efgredlem  16368  frgpup2  16397  frgpnabllem2  16476  frgpnabl  16477  ghmcyg  16496  gsumpt  16579  gsumptOLD  16580  gsummptfzcl  16585  dprdfadd  16635  dprdfeq0  16637  dprdfaddOLD  16642  dprdfeq0OLD  16644  dprdss  16651  subgdmdprd  16656  dprd2da  16666  dpjlem  16675  dpjf  16681  dpjidcl  16682  dpjlid  16685  dpjghm  16687  dpjghm2  16688  dpjidclOLD  16689  ablfac1b  16696  imasrng  16837  isabvd  17031  islmhm2  17245  lmhmplusg  17251  lmhmvsca  17252  lmhmpropd  17280  pj1lmhm  17307  fidomndrnglem  17504  psrmulcllem  17584  psrlidm  17600  psrlidmOLD  17601  psrridm  17602  psrridmOLD  17603  psrass1  17604  psrdi  17605  psrdir  17606  psrass23l  17607  psrcom  17608  psrass23  17609  resspsrmul  17616  mvrcl2  17626  mplsubrglem  17644  mplsubrglemOLD  17645  mplmonmul  17670  mplcoe1  17671  mplcoe5  17675  mplcoe2OLD  17677  subrgasclcl  17708  evlslem2  17724  evlslem6  17725  evlslem6OLD  17726  evlslem3  17727  evlslem1  17728  evlsval2  17733  mpfconst  17743  mpfind  17749  psropprmul  17819  coe1mul2  17849  coe1tmmul2  17856  coe1pwmul  17859  evls1val  17883  evls1sca  17886  fveval1fvcl  17895  evl1scad  17897  evl1addd  17903  evl1subd  17904  evl1muld  17905  evl1expd  17907  evl1scvarpw  17925  domnchr  18091  znidomb  18122  znrrg  18126  frgpcyg  18134  psgnodpm  18146  regsumsupp  18180  frlmssuvc1  18347  frlmssuvc2  18348  frlmssuvc1OLD  18349  frlmssuvc2OLD  18350  frlmsslsp  18351  frlmsslspOLD  18352  frlmup2  18355  lindfind2  18375  f1lindf  18379  mavmulcl  18488  mdetdiaglem  18539  mdetrlin  18543  mdetrsca  18544  mdetr0  18546  mdetero  18551  mdetunilem6  18558  mdetunilem7  18559  mdetunilem8  18560  mdetunilem9  18561  mdetuni0  18562  mdetmul  18564  maduf  18582  madutpos  18583  madugsum  18584  madurid  18585  madulid  18586  matinv  18618  matunit  18619  cramerimp  18627  iscnp4  19002  cnprest2  19029  lmcnp  19043  cnt0  19085  cnhaus  19093  ptpjopn  19320  ptcnplem  19329  pthaus  19346  xkohaus  19361  pt1hmeo  19514  ptcmpfi  19521  xkohmeo  19523  cnpflfi  19707  tmdgsum  19801  symgtgp  19807  ghmcnp  19820  imasdsf1olem  20083  imasf1obl  20198  comet  20223  metcnp3  20250  metcnp  20251  metcnp2  20252  metcnpi3  20256  metustexhalfOLD  20273  metustexhalf  20274  metucnOLD  20298  metucn  20299  nrmmetd  20302  nmoi2  20444  nmoco  20451  nmotri  20453  nmods  20458  nghmcn  20459  metds0  20561  metdstri  20562  metdsre  20564  metdscnlem  20566  metdscn  20567  metnrmlem1a  20569  metnrmlem1  20570  elcncf2  20601  cncfco  20618  cnheibor  20662  lebnumlem1  20668  lebnumlem3  20670  pi1cof  20766  pi1coghm  20768  nmoleub2lem  20804  nmoleub2lem3  20805  nmoleub3  20809  lmnn  20909  iscauf  20926  caucfil  20929  equivcau  20946  caubl  20953  caublcls  20954  lmcau  20958  rrxdstprj1  21043  pmltpclem2  21068  evthicc2  21079  ovoliunlem1  21120  ovoliunlem2  21121  ovolicc2lem1  21135  ovolicc2lem2  21136  ovolicc2lem3  21137  ovolicc2lem4  21138  volsup  21173  uniioombllem3  21201  volcn  21222  vitalilem2  21225  vitalilem3  21226  i1faddlem  21307  i1fmullem  21308  mbfi1fseqlem6  21334  mbfmullem2  21338  itg2monolem1  21364  limccnp  21502  dvlem  21507  dvcnp2  21530  dvaddbr  21548  dvmulbr  21549  dvcmul  21554  dvcobr  21556  dvcjbr  21559  dvcnvlem  21584  dvef  21588  dvferm1lem  21592  dvferm1  21593  dvferm2lem  21594  dvferm2  21595  dvferm  21596  rolle  21598  cmvth  21599  mvth  21600  dvlip  21601  dvlipcn  21602  c1liplem1  21604  dveq0  21608  dv11cn  21609  dvgt0  21612  dvlt0  21613  dvge0  21614  dvivthlem1  21616  dvivth  21618  lhop1lem  21621  lhop2  21623  dvcnvrelem1  21625  dvcnvrelem2  21626  dvcvx  21628  dvfsumlem3  21636  dvfsumrlim  21639  dvfsumrlim2  21640  ftc1a  21645  ftc1lem4  21647  ftc1lem5  21648  ftc1lem6  21649  ftc2  21652  ftc2ditg  21654  itgsubst  21657  tdeglem4  21665  mdegle0  21684  mdegmullem  21685  deg1ldgdomn  21701  deg1add  21711  deg1sublt  21718  deg1mul2  21722  deg1mul3  21723  deg1mul3le  21724  ply1nz  21729  ply1divex  21744  uc1pmon1p  21759  ply1remlem  21770  ply1rem  21771  facth1  21772  fta1glem1  21773  fta1glem2  21774  fta1g  21775  fta1blem  21776  drnguc1p  21778  ig1peu  21779  plyeq0lem  21814  dgrub  21838  coemullem  21853  coemulhi  21857  dgradd2  21871  dgrmul  21873  dgrcolem2  21877  plymul0or  21883  dvply1  21886  dvply2g  21887  plydivlem4  21898  vieta1lem2  21913  plyexmo  21915  elqaalem2  21922  elqaalem3  21923  aareccl  21928  aalioulem3  21936  aalioulem4  21937  taylfvallem1  21958  tayl0  21963  taylply2  21969  taylply  21970  dvtaylp  21971  taylthlem1  21974  taylthlem2  21975  ulmclm  21988  ulmshftlem  21990  ulmshft  21991  ulmcaulem  21995  ulmcau  21996  ulmbdd  21999  ulmcn  22000  ulmdvlem1  22001  mtest  22005  mtestbdd  22006  radcnvlem1  22014  pserulm  22023  psercn  22027  pserdvlem2  22029  abelthlem5  22036  abelthlem7  22039  abelthlem9  22041  abelth  22042  eff1olem  22140  efrlim  22499  scvxcvx  22515  jensenlem1  22516  jensenlem2  22517  jensen  22518  amgm  22520  ftalem1  22546  ftalem2  22547  ftalem3  22548  ftalem4  22549  ftalem5  22550  ftalem7  22552  dchrelbas3  22713  dchrzrhcl  22720  dchrzrhmul  22721  dchrn0  22725  dchrinvcl  22728  dchrabs  22735  dchrinv  22736  dchrptlem1  22739  dchrptlem2  22740  dchrsum2  22743  sumdchr2  22745  dchrhash  22746  sum2dchr  22749  bposlem3  22761  bposlem5  22763  bposlem6  22764  lgsval2lem  22781  lgsqrlem1  22816  lgsqrlem2  22817  lgsqrlem3  22818  lgsqrlem4  22819  lgseisenlem3  22826  lgseisenlem4  22827  rpvmasumlem  22872  dchrisumlem3  22876  dchrmusum2  22879  dchrvmasumlem3  22884  dchrvmasumiflem1  22886  dchrisum0ff  22892  dchrisum0flblem1  22893  dchrisum0flblem2  22894  rpvmasum2  22897  dchrisum0re  22898  dchrisum0lem1b  22900  mircl  23209  mirbtwni  23218  mirbtwnb  23219  mirauto  23222  miduniq2  23225  krippenlem  23228  lmicl  23278  f1otrg  23289  f1otrge  23290  axcontlem10  23391  wlkonwlk  23606  nvnencycllem  23701  eupap1  23769  eupath2lem3  23772  eupath2  23773  ghomid  24024  ghgrp  24027  lno0  24328  lnomul  24332  ubthlem2  24444  ubthlem3  24445  minvecolem3  24449  chscllem2  25213  chscllem3  25214  off2  26130  abliso  26324  gsumle  26411  rhmdvd  26454  kerunit  26456  tpr2rico  26507  lmdvg  26548  pl1cn  26550  qqhval2lem  26575  qqhf  26580  qqhghm  26582  qqhrhm  26583  qqhnm  26584  qqhcn  26585  qqhre  26611  esumfzf  26683  esumfsup  26684  esumpcvgval  26692  esumcocn  26694  esumcvg  26700  volmeas  26811  oms0  26874  omsmon  26875  eulerpartlemsv2  26905  eulerpartlemsf  26906  eulerpartlemsv3  26908  eulerpartlemv  26911  eulerpartlemf  26917  eulerpartlemgh  26925  eulerpartlemgs2  26927  sseqf  26939  sseqp1  26942  fiblem  26945  dstfrvel  27020  plymulx0  27112  plyrecld  27114  signsplypnf  27115  signsply0  27116  signstcl  27130  signstf  27131  signstfvn  27134  signsvtn0  27135  signsvtp  27148  signsvtn  27149  signsvfpn  27150  signsvfnn  27151  signlem0  27152  subfacp1lem5  27236  erdszelem7  27249  erdszelem8  27250  erdszelem9  27251  cvxscon  27296  cvmopnlem  27331  cvmfolem  27332  cvmliftmolem1  27334  cvmliftmolem2  27335  cvmliftlem1  27338  cvmliftlem6  27343  cvmliftlem7  27344  cvmlift2lem5  27360  cvmlift2lem7  27362  cvmlift2lem10  27365  cvmlift3lem6  27377  cvmlift3lem7  27378  cvmlift3lem9  27380  sinccvglem  27481  clim2prod  27567  clim2div  27568  prodrblem  27606  fprodcvg  27607  prodmolem2a  27611  fprodss  27625  iprodefisumlem  27668  heicant  28594  ftc1cnnclem  28633  ftc1cnnc  28634  ftc2nc  28644  f1ocan1fv  28788  sdclem2  28806  caushft  28825  heibor1lem  28876  bfplem1  28889  bfplem2  28890  rrndstprj1  28897  rrncmslem  28899  ismrcd1  29202  mzpindd  29250  diophin  29279  diophun  29280  mzpcong  29483  fnwe2lem3  29573  hbtlem2  29648  dgrsub2  29659  mpaaeu  29675  cnsrplycl  29692  idomrootle  29728  fmuldfeqlem1  29931  fmuldfeq  29932  stoweidlem3  29966  stoweidlem5  29968  stoweidlem11  29974  stoweidlem16  29979  stoweidlem17  29980  stoweidlem20  29983  stoweidlem22  29985  stoweidlem23  29986  stoweidlem24  29987  stoweidlem25  29988  stoweidlem26  29989  stoweidlem28  29991  stoweidlem32  29995  stoweidlem36  29999  stoweidlem42  30005  stoweidlem48  30011  stoweidlem51  30014  stoweidlem52  30015  stoweidlem59  30022  stirlinglem8  30044  stirlinglem15  30051  imarnf1pr  30318  lswn0  30426  wlkiswwlk1  30492  clwlkisclwwlklem1  30617  vdgfrgragt2  30788  coe1fzgsumdlem  31010  cply1coe0bi  31024  lply1binomsc  31030  linply1  31031  mat2pmatbas  31235  m2cpmfo  31261  pmatcollpw3fi1lem1  31293  mply1topmatcl  31312  cpscmat  31348  cpscmatgsumbin  31350  chfacfisf  31360  chfacfisfcpmat  31361  chfacfscmulcl  31363  chfacfscmulgsum  31366  chfacfpmmulcl  31367  chfacfpmmulgsum  31370  chfacfpmmulgsum2  31371  cayhamlem1  31372  cpmadugsumlemF  31382  cpmadugsumfi  31383  cayhamlem4  31395  lflcl  33067  tendocl  34769  lcfrlem13  35558  mapdcl  35656  hvmapclN  35767  hvmapcl2  35769
  Copyright terms: Public domain W3C validator