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

Theorem mpteq2dva 4663
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:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dva
StepHypRef Expression
1 nfv 1829 . 2 𝑥𝜑
2 mpteq2dva.1 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
31, 2mpteq2da 4662 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  cmpt 4634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-ral 2897  df-opab 4635  df-mpt 4636
This theorem is referenced by:  mpteq2dv  4664  2fvcoidd  6427  offval  6776  offval2  6786  caofinvl  6796  caofcom  6801  caofass  6803  caofdi  6805  caofdir  6806  caonncan  6807  curry1  7130  curry2  7133  mpt2curryd  7256  pw2f1olem  7923  mapxpen  7985  xpmapenlem  7986  cantnfp1  8435  cantnflem1d  8442  cantnflem1  8443  cnfcom2lem  8455  dfac12lem1  8822  seqof  12672  seqof2  12673  swrd0val  13216  swrdswrd  13255  repswswrd  13325  repswrevw  13327  revco  13374  ccatco  13375  repsco  13379  ofccat  13499  lo1eq  14090  rlimeq  14091  lo1mul2  14150  o1dif  14151  lo1sub  14152  rlimdiv  14167  caucvgr  14197  sumeq1  14210  fsumrlim  14327  fsumo1  14328  climfsum  14336  geomulcvg  14389  vdwlem8  15473  prmgapprmo  15547  restid2  15857  pwsplusgval  15916  pwsmulrval  15917  pwsvscafval  15920  qusin  15970  xpsaddlem  16001  xpsvsca  16005  catidd  16107  fuclid  16392  fucrid  16393  fucass  16394  setcepi  16504  prf1st  16610  prf2nd  16611  1st2ndprf  16612  curfcl  16638  curfuncf  16644  diag2  16651  curf2ndf  16653  hof2val  16662  hofcllem  16664  hofcl  16665  yonedalem4a  16681  yonedalem4c  16683  yonedalem3b  16685  yonedainv  16687  yonffthlem  16688  prdsidlem  17088  prdsmndd  17089  pwsco2mhm  17137  frmdup3lem  17169  frmdup3  17170  grpinvpropd  17256  prdsinvlem  17290  pwsinvg  17294  pwssub  17295  galactghm  17589  cayleylem1  17598  pmtrprfval  17673  sylow1lem2  17780  sylow3lem1  17808  efginvrel1  17907  frgpup3lem  17956  frgpup3  17957  prdscmnd  18030  iscyggen  18048  gsumval3  18074  gsumcllem  18075  gsumzsplit  18093  gsumsub  18114  gsummptf1o  18128  gsum2d  18137  gsum2d2  18139  gsumxp  18141  prdsgsum  18143  telgsumfz  18153  telgsumfz0  18155  telgsum  18157  dprdfsub  18186  dprdfeq0  18187  dprddisj2  18204  dprd2d2  18209  dpjidcl  18223  ablfaclem2  18251  ablfac2  18254  srgbinomlem3  18308  srgbinomlem4  18309  srgbinomlem  18310  gsumdixp  18375  prdsmgp  18376  prdsringd  18378  prdslmodd  18733  asclpropd  19110  psrass1lem  19141  psrlinv  19161  psrass1  19169  psrdi  19170  psrdir  19171  psrass23l  19172  psrcom  19173  psrass23  19174  resspsrmul  19181  mplsubrglem  19203  mplmonmul  19228  mplcoe1  19229  mplcoe5  19232  mplcoe4  19267  evlslem3  19278  evlslem1  19279  psrplusgpropd  19370  psropprmul  19372  coe1mul2  19403  coe1tm  19407  coe1tmmul2  19410  coe1tmmul  19411  coe1pwmul  19413  cply1mul  19428  ply1coe  19430  eqcoe1ply1eq  19431  lply1binomsc  19441  evl1gsummon  19493  mulgrhm2  19608  frgpcyg  19683  evpmodpmf1o  19703  phlpropd  19761  frlmphl  19878  uvcresum  19890  frlmup1  19895  mamures  19954  grpvrinv  19960  mhmvlin  19961  mamuass  19966  mamudi  19967  mamudir  19968  mamuvs1  19969  mamuvs2  19970  mpt2matmul  20010  mamutpos  20022  madetsumid  20025  dmatmul  20061  scmatscm  20077  1mavmul  20112  mavmulass  20113  mvmumamul1  20118  mulmarep1gsum1  20137  mulmarep1gsum2  20138  mdetleib2  20152  mdetfval1  20154  mdet0pr  20156  mdetdiag  20163  mdetdiagid  20164  mdetrlin  20166  mdetrsca  20167  mdetralt  20172  mdetunilem9  20184  gsummatr01  20223  smadiadetlem1a  20227  smadiadetlem3  20232  smadiadetlem4  20233  cpmatmcllem  20281  mat2pmatmul  20294  decpmatmullem  20334  decpmatmul  20335  pmatcollpw1lem2  20338  pmatcollpw  20344  pmatcollpw3lem  20346  pmatcollpwscmat  20354  idpm2idmp  20364  mp2pm2mplem3  20371  mp2pm2mplem4  20372  mp2pm2mplem5  20373  mp2pm2mp  20374  pm2mpghm  20379  pm2mpmhmlem2  20382  monmat2matmon  20387  pm2mp  20388  chpdmat  20404  chpscmat  20405  chpscmatgsumbin  20407  chpscmatgsummon  20408  chp0mat  20409  chpidmat  20410  chfacfscmulgsum  20423  chfacfpmmulgsum  20427  chfacfpmmulgsum2  20428  cayhamlem1  20429  cpmidgsumm2pm  20432  cpmidpmat  20436  cpmadugsumlemB  20437  cpmadugsumlemC  20438  cpmadugsumlemF  20439  cpmadumatpoly  20446  cayhamlem3  20450  cayhamlem4  20451  cayleyhamilton0  20452  cayleyhamiltonALT  20454  neiptopnei  20685  neiptopreu  20686  ptcnplem  21173  cnmpt1t  21217  cnmpt12  21219  cnmptkp  21232  cnmptk1  21233  cnmpt1k  21234  cnmptkk  21235  cnmptk1p  21237  cnmpt2k  21240  qtopeu  21268  pt1hmeo  21358  ptunhmeo  21360  xkocnv  21366  xkohmeo  21367  flfcnp2  21560  cnmpt1plusg  21640  istgp2  21644  tmdmulg  21645  tgpmulg  21646  tmdgsum  21648  symgtgp  21654  subgtgp  21658  tgpconcomp  21665  prdstgpd  21677  tsmsmhm  21698  tsmsadd  21699  tsmssub  21701  tgptsmscls  21702  tsmssplit  21704  tsmsxplem1  21705  tsmsxplem2  21706  cnmpt1vsca  21746  tlmtgp  21748  ustuqtoplem  21792  utopsnneip  21801  ressprdsds  21924  metuval  22102  nmfval2  22143  tngnm  22200  nmoeq0  22279  idnghm  22286  cnmpt1ds  22382  fsumcn  22409  expcn  22411  divccn  22412  divccncf  22445  negcncf  22457  copco  22554  pcopt  22558  pcopt2  22559  pcoass  22560  pi1xfrcnvlem  22592  cnmpt1ip  22769  rrxnm  22901  rrxds  22903  minveclem3b  22921  ovolctb  22979  ovoliunnul  22996  voliunlem3  23041  ovolfs2  23059  uniioombllem2  23071  vitalilem4  23100  vitalilem5  23101  ismbf  23117  mbfss  23133  mbfmulc2re  23135  mbfneg  23137  mbfpos  23138  mbfposb  23140  mbfadd  23148  mbfsub  23149  mbfmulc2  23150  mbfinf  23152  mbflimsup  23153  mbflimlem  23154  i1fpos  23193  i1fposd  23194  itg1climres  23201  mbfmul  23213  itg2mulc  23234  itg2i1fseq  23242  itg2cnlem1  23248  itg2cnlem2  23249  itgresr  23265  iblneg  23289  i1fibl  23294  itgitg1  23295  iblsub  23308  itgfsum  23313  itgmulc2lem1  23318  limcmpt  23367  limccnp  23375  limcco  23377  dvreslem  23393  dvres2lem  23394  dvidlem  23399  dvcnp2  23403  dvaddbr  23421  dvmulbr  23422  dvmulf  23426  dvcmulf  23428  dvcobr  23429  dvcof  23431  dvcjbr  23432  dvcj  23433  dvfre  23434  dvexp  23436  dvexp2  23437  dvrec  23438  dvmptcmul  23447  dvmptdivc  23448  dvmptneg  23449  dvmptsub  23450  dvmptre  23452  dvmptim  23453  dvmptfsum  23456  dvcnvlem  23457  dvcnv  23458  dvexp3  23459  dvef  23461  dvsincos  23462  dv11cn  23482  lhop2  23496  lhop  23497  ftc2  23525  itgparts  23528  itgsubstlem  23529  mdegfval  23540  mdegmullem  23556  ply1termlem  23677  plypow  23679  plyconst  23680  plyeq0lem  23684  plypf1  23686  plyaddlem1  23687  plymullem1  23688  coeeulem  23698  coeidlem  23711  plyco  23715  coeeq2  23716  0dgr  23719  0dgrb  23720  dgrcolem1  23747  dgrcolem2  23748  plycjlem  23750  dvply1  23757  dvply2g  23758  plydiveu  23771  plyremlem  23777  elqaalem3  23794  taylfval  23831  dvtaylp  23842  taylthlem1  23845  taylthlem2  23846  ulmshft  23862  mtestbdd  23877  iblulm  23879  itgulm2  23881  pserulm  23894  psercn2  23895  pserdvlem2  23900  pserdv  23901  pserdv2  23902  abelthlem1  23903  abelthlem3  23905  advlog  24114  advlogexp  24115  dvcxp1  24195  dvcxp2  24196  dvcncxp1  24198  sqrtcn  24205  loglesqrt  24213  dvatan  24376  atantayl2  24379  atantayl3  24380  leibpi  24383  rlimcnp2  24407  efrlim  24410  dfef2  24411  cxp2lim  24417  divsqrtsumlem  24420  lgamgulmlem2  24470  lgamgulm2  24476  lgamcvglem  24480  gamcvg2lem  24499  ftalem7  24519  basellem9  24529  muinv  24633  logfacrlim  24663  logexprlim  24664  dchrmulid2  24691  dchrinvcl  24692  lgseisenlem3  24816  lgseisenlem4  24817  chtppilimlem2  24877  chebbnd2  24880  chpchtlim  24882  chpo1ub  24883  rpvmasumlem  24890  dchrmusumlema  24896  dchrvmasumlem1  24898  dchrvmasumiflem2  24905  dchrisum0fno1  24914  rpvmasum2  24915  dchrisum0lema  24917  dchrisum0lem1  24919  dchrisum0lem2a  24920  dchrisum0lem2  24921  dchrisum0  24923  dchrmusumlem  24925  dchrvmasumlem  24926  rpvmasum  24929  rplogsum  24930  logdivsum  24936  mulog2sumlem3  24939  vmalogdivsum2  24941  vmalogdivsum  24942  2vmadivsumlem  24943  logsqvma2  24946  log2sumbnd  24947  selberglem2  24949  selberg3lem1  24960  selberg3  24962  selberg4lem1  24963  selberg4  24964  pntrsumo1  24968  selberg3r  24972  selberg4r  24973  selberg34r  24974  pntrlog2bndlem2  24981  pntrlog2bndlem4  24983  pntrlog2bndlem5  24984  pntrlog2bndlem6  24986  padicabvf  25034  padicabvcxp  25035  mirval  25265  wwlknprop  25977  chscllem4  27686  brafnmul  27997  kbmul  28001  ofresid  28627  ofoprabco  28650  fcobijfs  28692  gsummpt2d  28915  gsummptres  28918  fzto1st1  28986  fzto1st  28987  mdetpmtr1  29020  mdetlap  29029  xrge0mulc1cn  29118  esumval  29238  esumsnf  29256  esumpcvgval  29270  esumcvg  29278  esumcvgsum  29280  esumsup  29281  ofcfeqd2  29293  meascnbl  29412  sitgval  29524  probmeasb  29622  cndprobprob  29630  dstfrvclim1  29669  ballotlemfval  29681  ballotlemsval  29700  ballotlemieq  29708  plymul02  29752  plymulx0  29753  plymulx  29754  signsplypnf  29756  signstfv  29769  signstfvn  29775  signstfvp  29777  ptpcon  30272  cvmliftlem6  30329  cvmliftphtlem  30356  cvmlift3lem5  30362  elmrsubrn  30474  msubfval  30478  msubco  30485  divcnvlin  30674  knoppcnlem9  31464  knoppcnlem10  31465  knoppcnlem11  31466  bj-finsumval0  32124  curf  32357  matunitlindflem1  32375  matunitlindflem2  32376  poimirlem3  32382  poimirlem15  32394  poimirlem16  32395  poimirlem17  32396  poimirlem19  32398  poimirlem20  32399  broucube  32413  ovoliunnfl  32421  voliunnfl  32423  volsupnfl  32424  mbfposadd  32427  itg2addnclem  32431  itg2addnclem3  32433  itg2addnc  32434  itgaddnclem2  32439  itgaddnc  32440  iblsubnc  32441  itgsubnc  32442  itgmulc2nclem1  32446  itgmulc2nclem2  32447  itgmulc2nc  32448  itgabsnc  32449  ftc1cnnclem  32453  ftc1anclem3  32457  ftc1anclem5  32459  ftc1anclem6  32460  ftc1anclem8  32462  ftc1anc  32463  ftc2nc  32464  areacirclem1  32470  areacirclem2  32471  areacirclem4  32473  areacirc  32475  upixp  32494  mzpsubst  36129  mzprename  36130  mzpcompact2lem  36132  eldioph2  36143  rabdiophlem2  36184  mendlmod  36582  mendassa  36583  areaquad  36621  fsovcnvlem  37127  hashnzfzclim  37343  expgrowthi  37354  expgrowth  37356  uzmptshftfval  37367  dvradcnv2  37368  binomcxplemrat  37371  binomcxplemfrat  37372  binomcxplemradcnv  37373  binomcxplemdvbinom  37374  binomcxplemcvg  37375  binomcxplemdvsum  37376  binomcxplemnotnn0  37377  mulc1cncfg  38457  expcnfg  38459  fprodcnlem  38467  clim1fr1  38469  divcnvg  38495  sublimc  38520  reclimc  38521  divlimc  38524  cncfmptssg  38556  negcncfg  38567  divcncf  38570  cncficcgt0  38575  fprodcncf  38588  fprodsubrecnncnvlem  38595  fprodaddrecnncnvlem  38597  dvrecg  38601  dvsinax  38602  dvmptdiv  38608  dvasinbx  38611  dvdivf  38613  ioodvbdlimc1lem2  38623  ioodvbdlimc2lem  38625  dvnmptdivc  38629  dvxpaek  38631  dvnxpaek  38633  dvnmul  38634  dvnprodlem2  38638  ibliccsinexp  38643  itgsinexplem1  38646  itgsinexp  38647  iblempty  38658  itgcoscmulx  38662  itgsincmulx  38667  itgioocnicc  38670  iblcncfioo  38671  itgsbtaddcnst  38675  volioofmpt  38688  volicofmpt  38691  stoweidlem4  38698  stirlinglem5  38772  dirkerval  38785  dirkertrigeq  38795  dirkeritg  38796  dirkercncflem2  38798  dirkercncflem4  38800  fourierdlem16  38817  fourierdlem18  38819  fourierdlem21  38822  fourierdlem22  38823  fourierdlem28  38829  fourierdlem39  38840  fourierdlem40  38841  fourierdlem41  38842  fourierdlem53  38853  fourierdlem56  38856  fourierdlem57  38857  fourierdlem60  38860  fourierdlem61  38861  fourierdlem68  38868  fourierdlem73  38873  fourierdlem74  38874  fourierdlem75  38875  fourierdlem76  38876  fourierdlem78  38878  fourierdlem81  38881  fourierdlem82  38882  fourierdlem83  38883  fourierdlem84  38884  fourierdlem85  38885  fourierdlem88  38888  fourierdlem90  38890  fourierdlem92  38892  fourierdlem93  38893  fourierdlem95  38895  fourierdlem97  38897  fourierdlem101  38901  fourierdlem103  38903  fourierdlem104  38904  fourierdlem111  38911  fourierdlem112  38912  sqwvfoura  38922  sqwvfourb  38923  fouriersw  38925  elaa2lem  38927  etransclem4  38932  etransclem17  38945  etransclem18  38946  etransclem32  38960  etransclem46  38974  sge0z  39069  sge0revalmpt  39072  sge0tsms  39074  sge0sup  39085  sge0iunmptlemre  39109  sge0iun  39113  sge0xaddlem2  39128  ismeannd  39161  psmeasurelem  39164  meaiuninclem  39174  meaiininclem  39177  caratheodory  39219  isomenndlem  39221  ovnval  39232  hoicvrrex  39247  ovnlecvr  39249  ovncvrrp  39255  ovn0lem  39256  ovnsubaddlem1  39261  hoidmv1lelem2  39283  hoidmv1le  39285  hoidmvlelem3  39288  ovnhoilem2  39293  ovnhoi  39294  ovnlecvr2  39301  ovncvr2  39302  hspmbllem2  39318  ovolval2lem  39334  ovolval3  39338  ovolval5lem1  39343  ovolval5lem2  39344  ovnovollem1  39347  ovnovollem2  39348  vonioolem1  39372  vonicclem1  39375  vonct  39385  smflim  39464  crctcshlem4  41022  eucrct2eupth  41412  fdmdifeqresdif  41912  ply1mulgsumlem2  41968  lincvalsc0  42003  linc0scn0  42005  lincdifsn  42006  lincsum  42011  lincscm  42012  lindslinindimp2lem4  42043  lindslinindsimp2lem5  42044  lincresunit3lem2  42062  aacllem  42316  amgmwlem  42317
  Copyright terms: Public domain W3C validator