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

Theorem mpteq2dv 4778
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
Hypothesis
Ref Expression
mpteq2dv.1 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
mpteq2dv (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dv
StepHypRef Expression
1 mpteq2dv.1 . . 3 (𝜑𝐵 = 𝐶)
21adantr 480 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32mpteq2dva 4777 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  cmpt 4762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-opab 4746  df-mpt 4763
This theorem is referenced by:  ofeq  6941  mpt2curryvald  7441  rdgeq1  7552  rdgeq2  7553  omv  7637  oev  7639  oieq1  8458  oieq2  8459  cantnflem1  8624  wunex2  9598  wuncval2  9607  rpnnen1  11858  seqof2  12899  relexpsucnnr  13809  relexp1g  13810  limsupval  14249  sumeq2w  14466  sumeq2ii  14467  cbvsum  14469  summo  14492  fsum  14495  fsumrlim  14587  fsumo1  14588  prodeq2w  14686  prodmo  14710  fprod  14715  bpolylem  14823  rpnnen2lem1  14987  rpnnen2lem2  14988  1arithlem1  15674  vdwapval  15724  vdwlem6  15737  vdwlem8  15739  vdwlem9  15740  vdwlem10  15741  ramub1lem2  15778  ramcl  15780  sloteq  15909  prdsplusgval  16180  prdsmulrval  16182  prdsdsval  16185  prdsvscaval  16186  ismon  16440  fucco  16669  curf1  16912  curf2  16916  yonedalem4a  16962  grplactfval  17563  galactghm  17869  pmtrval  17917  sylow1  18064  sylow2b  18084  sylow3lem5  18092  sylow3  18094  iscyg  18327  gsumzaddlem  18367  gsumzmhm  18383  ablfac2  18534  gsumdixp  18655  fczpsrbag  19415  psrmulfval  19433  mvrval  19469  subrgmvr  19509  mplcoe1  19513  mplcoe3  19514  mplcoe5  19516  mplmon2  19541  subrgascl  19546  evlslem2  19560  evlslem3  19562  evlslem1  19563  mpfrcl  19566  evlsval  19567  evlsvar  19571  mpfind  19584  coe1fval  19623  pf1ind  19767  evl1gsumadd  19770  zncyg  19945  phllmhm  20025  isphld  20047  frlmgsum  20159  frlmipval  20166  frlmphl  20168  uvcval  20172  mamuval  20240  mamufv  20241  matgsum  20291  madetsumid  20315  mat1dimmul  20330  mvmulval  20397  mvmulfv  20398  mavmulfv  20400  1mavmul  20402  marepvval0  20420  mulmarep1gsum1  20427  mdetleib  20441  mdetleib2  20442  mdetfval1  20444  mdetleib1  20445  mdet0pr  20446  m1detdiag  20451  mdetralt  20462  mdetunilem9  20474  m2detleib  20485  smadiadetlem3  20522  mat2pmatmul  20584  decpmatmul  20625  decpmatmulsumfsupp  20626  pmatcollpw1  20629  monmatcollpw  20632  pmatcollpw3lem  20636  pmatcollpw3fi1lem2  20640  pm2mpval  20648  pm2mpfval  20649  mply1topmatval  20657  mp2pm2mplem1  20659  mp2pm2mplem3  20661  ptbasfi  21432  ptcnplem  21472  ptrescn  21490  cnmpt2k  21539  xkohmeo  21666  fmval  21794  fmf  21796  ptcmpg  21908  tmdmulg  21943  prdstmdd  21974  tsmspropd  21982  prdsxmslem2  22381  metdsval  22697  fsumcn  22720  expcn  22722  lebnumlem3  22809  pcoval  22857  pi1xfrcnv  22903  rrxds  23227  rrxmval  23234  itg11  23503  mbfi1fseqlem2  23528  mbfi1fseqlem6  23532  mbfi1fseq  23533  mbfi1flimlem  23534  mbfmullem  23537  itg2const  23552  itg2mulc  23559  itg2monolem1  23562  itg2i1fseqle  23566  itg2i1fseq  23567  itg2addlem  23570  itg2cnlem1  23573  itg2cn  23575  isibl  23577  isibl2  23578  iblitg  23580  itgz  23592  itgvallem  23596  itgvallem3  23597  iblcnlem1  23599  itgcnlem  23601  iblrelem  23602  iblposlem  23603  iblpos  23604  itgrevallem1  23606  itgposval  23607  iblss2  23617  itgss  23623  itgfsum  23638  iblabslem  23639  iblmulc2  23642  bddmulibl  23650  itgcn  23654  ellimc  23682  dvnfval  23730  cpnfval  23740  dvexp  23761  dvexp2  23762  dvmptfsum  23783  dvlipcn  23802  dvivthlem1  23816  dvfsumle  23829  dvfsumabs  23831  dvfsumlem2  23835  elply2  23997  elplyr  24002  elplyd  24003  coeeu  24026  coelem  24027  coeeq  24028  plyco  24042  coe11  24054  coe1termlem  24059  dgrcolem1  24074  dvply2g  24085  elqaalem3  24121  eltayl  24159  tayl0  24161  taylthlem1  24172  taylthlem2  24173  ulmcau  24194  ulmdvlem1  24199  ulmdvlem3  24201  mtest  24203  mtestbdd  24204  pserval  24209  pserulm  24221  psercn  24225  pserdvlem2  24227  abelthlem3  24232  logtayl  24451  dvcxp1  24526  dvcncxp1  24529  logbmpt  24571  dmarea  24729  lgamgulmlem2  24801  lgamgulmlem5  24804  musum  24962  dchrptlem2  25035  dchrptlem3  25036  dchrpt  25037  lgsval  25071  lgsval4lem  25078  lgsneg  25091  lgsmod  25093  rpvmasum2  25246  padicfval  25350  ostth2  25371  ostth3  25372  ostth  25373  lmif  25722  islmib  25724  incistruhgr  26019  eucrct2eupth  27223  htthlem  27902  htth  27903  pjhfval  28383  hosmval  28722  hommval  28723  hodmval  28724  hfsmval  28725  hfmmval  28726  brafval  28930  kbfval  28939  psgnfzto1st  29983  mdetpmtr1  30017  ordtcnvNEW  30094  ordtrest2NEW  30097  xrhval  30190  indval  30203  esum2dlem  30282  ofceq  30287  itgeq12dv  30516  ballotlemfval  30679  vtsval  30843  ptpconn  31341  cvmliftlem15  31406  cvmlift2lem4  31414  cvmlift2  31424  snmlval  31439  snmlflim  31440  mrsubfval  31531  mrsubrn  31536  elmsubrn  31551  msubrn  31552  msubco  31554  faclim  31758  faclim2  31760  trpredeq1  31844  trpredeq2  31845  knoppcnlem1  32608  knoppcnlem6  32613  knoppcnlem7  32614  bj-evaleq  33149  csbrdgg  33305  curfv  33519  matunitlindflem2  33536  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem27  33566  voliunnfl  33583  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  iblabsnclem  33603  iblmulc2nc  33605  ftc1anclem2  33616  ftc1anclem6  33620  ftc1anclem8  33622  ftc1anc  33623  ftc2nc  33624  upixp  33654  rrncmslem  33761  ismrer1  33767  tendoplcbv  36380  tendopl  36381  tendoicbv  36398  tendoi  36399  dihfval  36837  lcfl7N  37107  lcfrlem8  37155  lcfrlem9  37156  lcf1o  37157  hvmapval  37366  hdmap1fval  37403  hdmapffval  37435  hdmapfval  37436  hgmapffval  37494  hgmapfval  37495  mzpclval  37605  mzpcl2  37610  mzpexpmpt  37625  mzpsubst  37628  mzpcompact2lem  37631  rmxfval  37785  rmyfval  37786  aomclem8  37948  hbtlem1  38010  hbtlem7  38012  itgpowd  38117  rfovfvd  38613  fsovrfovd  38620  fsovfvd  38621  fsovcnvlem  38624  dssmapfv2d  38629  dssmapnvod  38631  ntrneibex  38688  expgrowthi  38849  expgrowth  38851  binomcxplemdvsum  38871  addrval  38987  subrval  38988  mulvval  38989  fmulcl  40131  fmuldfeqlem1  40132  fprodcnlem  40149  fprodcn  40150  fnlimfv  40213  fnlimcnv  40217  fnlimfvre  40224  fnlimfvre2  40227  fnlimf  40228  fnlimabslt  40229  liminfval  40309  limsupresxr  40316  liminfresxr  40317  liminfvalxr  40333  fprodcncf  40432  dvnmptdivc  40471  dvnxpaek  40475  dvnmul  40476  dvmptfprod  40478  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  dvnprod  40482  stoweidlem2  40537  stoweidlem17  40552  stoweidlem19  40554  stoweidlem20  40555  stoweidlem43  40578  stoweidlem62  40597  stoweid  40598  dirkercncflem2  40639  fourierdlem112  40753  fourierdlem113  40754  etransclem1  40770  etransclem5  40774  etransclem17  40786  etransclem19  40788  etransclem22  40791  sge0val  40901  ovnlecvr  41093  ovncvrrp  41099  ovn0lem  41100  ovnsubaddlem1  41105  ovnsubadd  41107  hsphoif  41111  hsphoival  41114  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoidmvlelem5  41134  hoidmvle  41135  ovnhoilem1  41136  ovnhoi  41138  hoidifhspval  41143  ovncvr2  41146  hoidifhspval2  41150  hspmbllem2  41162  hspmbllem3  41163  hspmbl  41164  ovnovollem1  41191  vonioolem2  41216  vonioo  41217  vonicclem2  41219  vonicc  41220  smflimlem4  41303  smflim  41306  smflim2  41333  smfsuplem2  41339  smfsup  41341  smfinf  41345  smflimsuplem2  41348  smflimsuplem5  41351  smflimsuplem7  41353  smflimsup  41355  c0rhm  42237  c0rnghm  42238  lincop  42522  aacllem  42875
  Copyright terms: Public domain W3C validator