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

Theorem fvmptg 5954
Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fvmptg.1
fvmptg.2
Assertion
Ref Expression
fvmptg
Distinct variable groups:   ,   ,   ,

Proof of Theorem fvmptg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2457 . 2
2 fvmptg.1 . . . 4
32eqeq2d 2471 . . 3
4 eqeq1 2461 . . 3
5 moeq 3275 . . . 4
65a1i 11 . . 3
7 fvmptg.2 . . . 4
8 df-mpt 4512 . . . 4
97, 8eqtri 2486 . . 3
103, 4, 6, 9fvopab3ig 5953 . 2
111, 10mpi 17 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  E*wmo 2283  {copab 4509  e.cmpt 4510  `cfv 5593
This theorem is referenced by:  fvmpti  5955  fvmpt  5956  fvtresfn  5957  fvmpts  5958  fvmpt3  5959  fvmptss2  5975  f1mpt  6169  undefval  7024  tz7.44-2  7092  tz7.44-3  7093  fvdiagfn  7483  resixpfo  7527  pw2f1olem  7641  fival  7892  wdom2d  8027  cantnfp1lem1  8118  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnfp1lem1OLD  8144  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  wemapwe  8160  wemapweOLD  8161  tz9.12lem3  8228  rankvalb  8236  cardval3  8354  cfval  8648  coftr  8674  fin23lem27  8729  isf34lem1  8773  fin1a2lem1  8801  fin1a2lem12  8812  axdc2lem  8849  pwcfsdom  8979  canthp1lem2  9052  wuncval  9141  tskmval  9238  lsw  12585  swrdswrd  12685  climrlim2  13370  summolem3  13536  summolem2a  13537  prodmolem3  13740  prodmolem2a  13741  iprodmul  13796  iserodd  14359  divsfval  14944  mreacs  15055  joinfval  15631  meetfval  15645  pwsco1mhm  16001  pwsco2mhm  16002  vrmdfval  16024  galactghm  16428  symgextfv  16443  symgextfve  16444  symgfixfolem1  16463  pmtrval  16476  pmtrfv  16477  pmtrdifwrdel2lem1  16509  efgtf  16740  gsummhm2  16961  gsummhm2OLD  16962  gsummpt1n0  16992  dprdfid  17057  dprdfidOLD  17064  lspval  17621  rrgsupp  17939  aspval  17977  evlslem3  18183  coe1tmfv1  18315  coe1tmfv2  18316  ply1sclid  18329  uvcval  18816  uvcvval  18817  marepvval  19069  submaval0  19082  m2detleiblem3  19131  m2detleiblem4  19132  maduval  19140  minmar1val0  19149  tgval  19456  cldval  19524  ntrfval  19525  clsfval  19526  ntrval  19537  clsval  19538  opncldf2  19586  opncldf3  19587  neifval  19600  neival  19603  lpfval  19639  lpval  19640  1stcfb  19946  islocfin  20018  cnmpt11  20164  cnmpt21  20172  cnmptkp  20181  cnmptk1p  20186  kqfval  20224  stdbdxmet  21018  cmetcaulem  21727  bcth3  21770  iunmbl  21963  itg2gt0  22167  ellimc2  22281  cnmptlimc  22294  limccnp  22295  limcco  22297  coe1termlem  22655  coe1term  22656  ulmval  22775  pserulm  22817  rlimcnp  23295  xrlimcnp  23298  dchrelbasd  23514  nbgraf1olem4  24444  fargshiftfv  24635  wwlkn  24682  clwwlkn  24767  clwlkfoclwwlk  24845  clwlkf1clwwlk  24850  rusgranumwlklem1  24949  usg2spot2nb  25065  usgreg2spot  25067  2spotmdisj  25068  usgreghash2spot  25069  numclwlk1lem2fv  25093  numclwlk2lem2fv  25104  grpoinvfval  25226  grpodivfval  25244  gxfval  25259  issubgo  25305  spanval  26251  nlfnval  26800  fvmpt2f  27498  sigaval  28110  measval  28169  measdivcstOLD  28195  measdivcst  28196  probfinmeasbOLD  28367  ptpcon  28678  cvmsval  28711  dfrtrclrec2  29066  rtrclreclem.refl  29067  climlec3  29120  bdayval  29408  imageval  29580  fvimage  29581  tailfval  30190  tailval  30191  heiborlem4  30310  heiborlem6  30312  mzpval  30664  mzpsubst  30681  rabdiophlem2  30735  fphpdo  30751  monotoddzz  30879  pw2f1o2val  30981  dnnumch3lem  30992  pwssplit4  31035  hbtlem1  31072  rgspnval  31117  refsum2cnlem1  31412  fmuldfeq  31577  cncfiooicclem1  31696  stoweidlem26  31808  stoweidlem30  31812  stoweidlem31  31813  stoweidlem34  31816  stirlinglem5  31860  stirlinglem8  31863  fourierdlem50  31939  lincvalsc0  33022  linc0scn0  33024  linc1  33026  lincscm  33031  el0ldep  33067  bj-diagval  34605  lkrval  34813  pclvalN  35614  cdleme31fv  36116  docavalN  36850  dochval  37078  mapdval  37355  hvmapval  37487  hvmapvalvalN  37488  hdmap1vallem  37525  hdmapval  37558  hgmapval  37617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fv 5601
  Copyright terms: Public domain W3C validator