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

Theorem mpteq2dva 4538
Description: Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
Hypothesis
Ref Expression
mpteq2dva.1
Assertion
Ref Expression
mpteq2dva
Distinct variable group:   ,

Proof of Theorem mpteq2dva
StepHypRef Expression
1 nfv 1707 . 2
2 mpteq2dva.1 . 2
31, 2mpteq2da 4537 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  e.cmpt 4510
This theorem is referenced by:  mpteq2dv  4539  2fvcoidd  6200  offval  6547  offval2  6556  caofinvl  6567  caofcom  6572  caofass  6574  caofdi  6576  caofdir  6577  caonncan  6578  curry1  6892  curry2  6895  mpt2curryd  7017  pw2f1olem  7641  mapxpen  7703  xpmapenlem  7704  cantnfp1  8121  cantnflem1d  8128  cantnflem1  8129  cantnfp1OLD  8147  cantnflem1dOLD  8151  cantnflem1OLD  8152  cnfcom2lem  8166  cnfcom2lemOLD  8174  dfac12lem1  8544  seqof  12164  seqof2  12165  swrd0val  12648  swrdswrd  12685  repswswrd  12756  repswrevw  12758  revco  12800  ccatco  12801  repsco  12805  lo1eq  13391  rlimeq  13392  lo1mul2  13451  o1dif  13452  lo1sub  13453  rlimdiv  13468  caucvgr  13498  sumeq1  13511  fsumrlim  13625  fsumo1  13626  climfsum  13634  geomulcvg  13685  vdwlem8  14506  restid2  14828  pwsplusgval  14887  pwsmulrval  14888  pwsvscafval  14891  qusin  14941  xpsaddlem  14972  xpsvsca  14976  catidd  15077  fuclid  15335  fucrid  15336  fucass  15337  setcepi  15415  prf1st  15473  prf2nd  15474  1st2ndprf  15475  curfcl  15501  curfuncf  15507  diag2  15514  curf2ndf  15516  hof2val  15525  hofcllem  15527  hofcl  15528  yonedalem4a  15544  yonedalem4c  15546  yonedalem3b  15548  yonedainv  15550  yonffthlem  15551  prdsidlem  15952  prdsmndd  15953  pwsco2mhm  16002  frmdup3lem  16034  frmdup3  16035  grpinvpropd  16113  prdsinvlem  16178  pwsinvg  16182  pwssub  16183  galactghm  16428  cayleylem1  16437  pmtrprfval  16512  sylow1lem2  16619  sylow3lem1  16647  efginvrel1  16746  frgpup3lem  16795  frgpup3  16796  prdscmnd  16867  iscyggen  16883  gsumval3OLD  16908  gsumval3  16911  gsumcllem  16912  gsumcllemOLD  16913  gsumzsplit  16944  gsumzsplitOLD  16945  gsumsub  16974  gsumsubOLD  16975  gsummptf1o  16990  gsum2d  16999  gsum2dOLD  17000  gsum2d2  17002  gsumxp  17004  gsumxpOLD  17006  prdsgsum  17007  prdsgsumOLD  17008  telgsumfz  17019  telgsumfz0  17021  telgsum  17023  dprdfsub  17061  dprdfeq0  17062  dprdfsubOLD  17068  dprdfeq0OLD  17069  dprddisj2  17087  dprddisj2OLD  17088  dprd2d2  17093  dpjidcl  17107  dpjidclOLD  17114  ablfaclem2  17137  ablfac2  17140  srgbinomlem3  17193  srgbinomlem4  17194  srgbinomlem  17195  gsumdixpOLD  17257  gsumdixp  17258  prdsmgp  17259  prdsringd  17261  prdslmodd  17615  asclpropd  17995  psrass1lem  18029  psrlinv  18050  psrass1  18060  psrdi  18061  psrdir  18062  psrass23l  18063  psrcom  18064  psrass23  18065  resspsrmul  18072  mplsubrglem  18100  mplsubrglemOLD  18101  mplmonmul  18126  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  mplcoe4  18168  evlslem3  18183  evlslem1  18184  psrplusgpropd  18277  psropprmul  18279  coe1mul2  18310  coe1tm  18314  coe1tmmul2  18317  coe1tmmul  18318  coe1pwmul  18320  cply1mul  18335  ply1coe  18337  ply1coeOLD  18338  eqcoe1ply1eq  18339  lply1binomsc  18349  evl1gsummon  18401  mulgrhm2  18533  mulgrhm2OLD  18536  frgpcyg  18612  evpmodpmf1o  18632  phlpropd  18690  frlmphl  18812  uvcresum  18824  frlmup1  18832  mamures  18892  grpvrinv  18898  mhmvlin  18899  mamuass  18904  mamudi  18905  mamudir  18906  mamuvs1  18907  mamuvs2  18908  mpt2matmul  18948  mamutpos  18960  madetsumid  18963  dmatmul  18999  scmatscm  19015  1mavmul  19050  mavmulass  19051  mvmumamul1  19056  mulmarep1gsum1  19075  mulmarep1gsum2  19076  mdetleib2  19090  mdetfval1  19092  mdet0pr  19094  mdetdiag  19101  mdetdiagid  19102  mdetrlin  19104  mdetrsca  19105  mdetralt  19110  mdetunilem9  19122  gsummatr01  19161  smadiadetlem1a  19165  smadiadetlem3  19170  smadiadetlem4  19171  cpmatmcllem  19219  mat2pmatmul  19232  decpmatmullem  19272  decpmatmul  19273  pmatcollpw1lem2  19276  pmatcollpw  19282  pmatcollpw3lem  19284  pmatcollpwscmat  19292  idpm2idmp  19302  mp2pm2mplem3  19309  mp2pm2mplem4  19310  mp2pm2mplem5  19311  mp2pm2mp  19312  pm2mpghm  19317  pm2mpmhmlem2  19320  monmat2matmon  19325  pm2mp  19326  chpdmat  19342  chpscmat  19343  chpscmatgsumbin  19345  chpscmatgsummon  19346  chp0mat  19347  chpidmat  19348  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  chfacfpmmulgsum2  19366  cayhamlem1  19367  cpmidgsumm2pm  19370  cpmidpmat  19374  cpmadugsumlemB  19375  cpmadugsumlemC  19376  cpmadugsumlemF  19377  cpmadumatpoly  19384  cayhamlem3  19388  cayhamlem4  19389  cayleyhamilton0  19390  cayleyhamiltonALT  19392  neiptopnei  19633  neiptopreu  19634  ptcnplem  20122  cnmpt1t  20166  cnmpt12  20168  cnmptkp  20181  cnmptk1  20182  cnmpt1k  20183  cnmptkk  20184  cnmptk1p  20186  cnmpt2k  20189  qtopeu  20217  pt1hmeo  20307  ptunhmeo  20309  xkocnv  20315  xkohmeo  20316  flfcnp2  20508  cnmpt1plusg  20586  istgp2  20590  tmdmulg  20591  tgpmulg  20592  tmdgsum  20594  symgtgp  20600  subgtgp  20604  tgpconcomp  20611  prdstgpd  20623  tsmsmhm  20648  tsmsadd  20649  tsmssub  20651  tgptsmscls  20652  tsmssplit  20654  tsmsxplem1  20655  tsmsxplem2  20656  cnmpt1vsca  20696  tlmtgp  20698  ustuqtoplem  20742  utopsnneip  20751  ressprdsds  20874  metuvalOLD  21052  metuval  21053  nmfval2  21111  tngnm  21165  nmoeq0  21243  idnghm  21250  cnmpt1ds  21347  fsumcn  21374  expcn  21376  divccn  21377  divccncf  21410  negcncf  21422  copco  21518  pcopt  21522  pcopt2  21523  pcoass  21524  pi1xfrcnvlem  21556  cnmpt1ip  21687  rrxnm  21823  rrxds  21825  minveclem3b  21843  ovolctb  21901  ovoliunnul  21918  voliunlem3  21962  ovolfs2  21980  uniioombllem2  21992  vitalilem4  22020  vitalilem5  22021  ismbf  22037  mbfss  22053  mbfmulc2re  22055  mbfneg  22057  mbfpos  22058  mbfposb  22060  mbfadd  22068  mbfsub  22069  mbfmulc2  22070  mbfinf  22072  mbflimsup  22073  mbflimlem  22074  i1fpos  22113  i1fposd  22114  itg1climres  22121  mbfmul  22133  itg2mulc  22154  itg2i1fseq  22162  itg2cnlem1  22168  itg2cnlem2  22169  itgresr  22185  iblneg  22209  i1fibl  22214  itgitg1  22215  iblsub  22228  itgfsum  22233  itgmulc2lem1  22238  limcmpt  22287  limccnp  22295  limcco  22297  dvreslem  22313  dvres2lem  22314  dvidlem  22319  dvcnp2  22323  dvaddbr  22341  dvmulbr  22342  dvmulf  22346  dvcmulf  22348  dvcobr  22349  dvcof  22351  dvcjbr  22352  dvcj  22353  dvfre  22354  dvexp  22356  dvexp2  22357  dvrec  22358  dvmptcmul  22367  dvmptdivc  22368  dvmptneg  22369  dvmptsub  22370  dvmptre  22372  dvmptim  22373  dvmptfsum  22376  dvcnvlem  22377  dvcnv  22378  dvexp3  22379  dvef  22381  dvsincos  22382  dv11cn  22402  lhop2  22416  lhop  22417  ftc2  22445  itgparts  22448  itgsubstlem  22449  mdegfval  22460  mdegmullem  22478  ply1termlem  22600  plypow  22602  plyconst  22603  plyeq0lem  22607  plypf1  22609  plyaddlem1  22610  plymullem1  22611  coeeulem  22621  coeidlem  22634  plyco  22638  coeeq2  22639  0dgr  22642  0dgrb  22643  dgrcolem1  22670  dgrcolem2  22671  plycjlem  22673  dvply1  22680  dvply2g  22681  plydiveu  22694  plyremlem  22700  elqaalem3  22717  taylfval  22754  dvtaylp  22765  taylthlem1  22768  taylthlem2  22769  ulmshft  22785  mtestbdd  22800  iblulm  22802  itgulm2  22804  pserulm  22817  psercn2  22818  pserdvlem2  22823  pserdv  22824  pserdv2  22825  abelthlem1  22826  abelthlem3  22828  advlog  23035  advlogexp  23036  dvcxp1  23116  dvcxp2  23117  sqrtcn  23124  loglesqrt  23132  dvatan  23266  atantayl2  23269  atantayl3  23270  leibpi  23273  rlimcnp2  23296  efrlim  23299  dfef2  23300  cxp2lim  23306  divsqrtsumlem  23309  ftalem7  23352  basellem9  23362  muinv  23469  logfacrlim  23499  logexprlim  23500  dchrmulid2  23527  dchrinvcl  23528  lgseisenlem3  23626  lgseisenlem4  23627  chtppilimlem2  23659  chebbnd2  23662  chpchtlim  23664  chpo1ub  23665  rpvmasumlem  23672  dchrmusumlema  23678  dchrvmasumlem1  23680  dchrvmasumiflem2  23687  dchrisum0fno1  23696  rpvmasum2  23697  dchrisum0lema  23699  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  dchrisum0  23705  dchrmusumlem  23707  dchrvmasumlem  23708  rpvmasum  23711  rplogsum  23712  logdivsum  23718  mulog2sumlem3  23721  vmalogdivsum2  23723  vmalogdivsum  23724  2vmadivsumlem  23725  logsqvma2  23728  log2sumbnd  23729  selberglem2  23731  selberg3lem1  23742  selberg3  23744  selberg4lem1  23745  selberg4  23746  pntrsumo1  23750  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntrlog2bndlem2  23763  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  padicabvf  23816  padicabvcxp  23817  mirval  24036  wwlknprop  24686  chscllem4  26558  brafnmul  26870  kbmul  26874  ofresid  27482  ofoprabco  27505  fcobijfs  27549  xrge0mulc1cn  27923  esumval  28057  esumsn  28072  esumpcvgval  28084  esumcvg  28092  ofcfeqd2  28100  meascnbl  28190  sitgval  28274  probmeasb  28369  cndprobprob  28377  dstfrvclim1  28416  ballotlemfval  28428  ballotlemsval  28447  ballotlemieq  28455  ofccat  28497  plymul02  28503  plymulx0  28504  plymulx  28505  signsplypnf  28507  signstfv  28520  signstfvn  28526  signstfvp  28528  lgamgulmlem2  28572  lgamgulm2  28578  lgamcvglem  28582  gamcvg2lem  28601  ptpcon  28678  cvmliftlem6  28735  cvmliftphtlem  28762  cvmlift3lem5  28768  elmrsubrn  28880  msubfval  28884  msubco  28891  divcnvlin  29118  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  mbfposadd  30062  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  itgaddnclem2  30074  itgaddnc  30075  iblsubnc  30076  itgsubnc  30077  itgmulc2nclem1  30081  itgmulc2nclem2  30082  itgmulc2nc  30083  itgabsnc  30084  ftc1cnnclem  30088  ftc1anclem3  30092  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem8  30097  ftc1anc  30098  ftc2nc  30099  dvcncxp1  30100  areacirclem1  30107  areacirclem2  30108  areacirclem4  30110  areacirc  30112  upixp  30220  mzpsubst  30681  mzprename  30682  mzpcompact2lem  30684  eldioph2  30695  rabdiophlem2  30735  mendlmod  31142  mendassa  31143  areaquad  31184  hashnzfzclim  31227  expgrowthi  31238  expgrowth  31240  uzmptshftfval  31251  dvradcnv2  31252  binomcxplemrat  31255  binomcxplemfrat  31256  binomcxplemradcnv  31257  binomcxplemdvbinom  31258  binomcxplemcvg  31259  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  mulc1cncfg  31583  expcnfg  31586  clim1fr1  31607  divcnvg  31633  sublimc  31658  reclimc  31659  divlimc  31662  cncfmptssg  31672  negcncfg  31683  divcncf  31686  cncficcgt0  31691  fprodcncf  31704  dvrecg  31707  dvsinax  31708  dvmptdiv  31714  dvasinbx  31717  dvdivf  31719  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnmptdivc  31735  dvxpaek  31737  dvnxpaek  31739  dvnmul  31740  dvnprodlem2  31744  ibliccsinexp  31749  itgsinexplem1  31752  itgsinexp  31753  iblempty  31764  itgcoscmulx  31768  itgsincmulx  31773  itgioocnicc  31776  iblcncfioo  31777  itgsbtaddcnst  31781  stoweidlem4  31786  stirlinglem5  31860  dirkerval  31873  dirkertrigeq  31883  dirkeritg  31884  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem16  31905  fourierdlem18  31907  fourierdlem21  31910  fourierdlem22  31911  fourierdlem28  31917  fourierdlem39  31928  fourierdlem40  31929  fourierdlem41  31930  fourierdlem53  31942  fourierdlem56  31945  fourierdlem57  31946  fourierdlem60  31949  fourierdlem61  31950  fourierdlem68  31957  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem81  31970  fourierdlem82  31971  fourierdlem83  31972  fourierdlem84  31973  fourierdlem85  31974  fourierdlem88  31977  fourierdlem90  31979  fourierdlem92  31981  fourierdlem93  31982  fourierdlem95  31984  fourierdlem97  31986  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  elaa2lem  32016  etransclem4  32021  etransclem17  32034  etransclem18  32035  etransclem32  32049  etransclem46  32063  fdmdifeqresdif  32931  ply1mulgsumlem2  32987  lincvalsc0  33022  linc0scn0  33024  lincdifsn  33025  lincsum  33030  lincscm  33031  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  lincresunit3lem2  33081  aacllem  33216  bj-finsumval0  34663
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-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-opab 4511  df-mpt 4512
  Copyright terms: Public domain W3C validator