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

Theorem mpteq2dv 4667
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 479 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32mpteq2dva 4666 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  cmpt 4637
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 2033  ax-13 2233  ax-ext 2589
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 2596  df-cleq 2602  df-clel 2605  df-ral 2900  df-opab 4638  df-mpt 4639
This theorem is referenced by:  ofeq  6774  mpt2curryvald  7260  rdgeq1  7371  rdgeq2  7372  omv  7456  oev  7458  oieq1  8277  oieq2  8278  cantnflem1  8446  wunex2  9416  wuncval2  9425  rpnnen1  11654  seqof2  12678  relexpsucnnr  13561  relexp1g  13562  limsupval  14001  sumeq2w  14218  sumeq2ii  14219  cbvsum  14221  summo  14243  fsum  14246  fsumrlim  14332  fsumo1  14333  prodeq2w  14429  prodmo  14453  fprod  14458  bpolylem  14566  rpnnen2lem1  14730  rpnnen2lem2  14731  1arithlem1  15413  vdwapval  15463  vdwlem6  15476  vdwlem8  15478  vdwlem9  15479  vdwlem10  15480  ramub1lem2  15517  ramcl  15519  prdsplusgval  15904  prdsmulrval  15906  prdsdsval  15909  prdsvscaval  15910  ismon  16164  fucco  16393  curf1  16636  curf2  16640  yonedalem4a  16686  grplactfval  17287  galactghm  17594  pmtrval  17642  sylow1  17789  sylow2b  17809  sylow3lem5  17817  sylow3  17819  iscyg  18052  gsumzaddlem  18092  gsumzmhm  18108  ablfac2  18259  gsumdixp  18380  fczpsrbag  19136  psrmulfval  19154  mvrval  19190  subrgmvr  19230  mplcoe1  19234  mplcoe3  19235  mplcoe5  19237  mplmon2  19262  subrgascl  19267  evlslem2  19281  evlslem3  19283  evlslem1  19284  mpfrcl  19287  evlsval  19288  evlsvar  19292  mpfind  19305  coe1fval  19344  pf1ind  19488  evl1gsumadd  19491  zncyg  19663  phllmhm  19743  isphld  19765  frlmgsum  19877  frlmipval  19884  frlmphl  19886  uvcval  19890  mamuval  19958  mamufv  19959  matgsum  20009  madetsumid  20033  mat1dimmul  20048  mvmulval  20115  mvmulfv  20116  mavmulfv  20118  1mavmul  20120  marepvval0  20138  mulmarep1gsum1  20145  mdetleib  20159  mdetleib2  20160  mdetfval1  20162  mdetleib1  20163  mdet0pr  20164  m1detdiag  20169  mdetralt  20180  mdetunilem9  20192  m2detleib  20203  smadiadetlem3  20240  mat2pmatmul  20302  decpmatmul  20343  decpmatmulsumfsupp  20344  pmatcollpw1  20347  monmatcollpw  20350  pmatcollpw3lem  20354  pmatcollpw3fi1lem2  20358  pm2mpval  20366  pm2mpfval  20367  mply1topmatval  20375  mp2pm2mplem1  20377  mp2pm2mplem3  20379  ptbasfi  21141  ptcnplem  21181  ptrescn  21199  cnmpt2k  21248  xkohmeo  21375  fmval  21504  fmf  21506  ptcmpg  21618  tmdmulg  21653  prdstmdd  21684  tsmspropd  21692  prdsxmslem2  22091  metdsval  22405  fsumcn  22428  expcn  22430  lebnumlem3  22517  pcoval  22566  pi1xfrcnv  22612  rrxds  22933  rrxmval  22940  itg11  23208  mbfi1fseqlem2  23233  mbfi1fseqlem6  23237  mbfi1fseq  23238  mbfi1flimlem  23239  mbfmullem  23242  itg2const  23257  itg2mulc  23264  itg2monolem1  23267  itg2i1fseqle  23271  itg2i1fseq  23272  itg2addlem  23275  itg2cnlem1  23278  itg2cn  23280  isibl  23282  isibl2  23283  iblitg  23285  itgz  23297  itgvallem  23301  itgvallem3  23302  iblcnlem1  23304  itgcnlem  23306  iblrelem  23307  iblposlem  23308  iblpos  23309  itgrevallem1  23311  itgposval  23312  iblss2  23322  itgss  23328  itgfsum  23343  iblabslem  23344  iblmulc2  23347  bddmulibl  23355  itgcn  23359  ellimc  23387  dvnfval  23435  cpnfval  23445  dvexp  23466  dvexp2  23467  dvmptfsum  23486  dvlipcn  23505  dvivthlem1  23519  dvfsumle  23532  dvfsumabs  23534  dvfsumlem2  23538  elply2  23700  elplyr  23705  elplyd  23706  coeeu  23729  coelem  23730  coeeq  23731  plyco  23745  coe11  23757  coe1termlem  23762  dgrcolem1  23777  dvply2g  23788  elqaalem3  23824  eltayl  23862  tayl0  23864  taylthlem1  23875  taylthlem2  23876  ulmcau  23897  ulmdvlem1  23902  ulmdvlem3  23904  mtest  23906  mtestbdd  23907  pserval  23912  pserulm  23924  psercn  23928  pserdvlem2  23930  abelthlem3  23935  logtayl  24150  dvcxp1  24225  dvcncxp1  24228  logbmpt  24270  dmarea  24428  lgamgulmlem2  24500  lgamgulmlem5  24503  musum  24661  dchrptlem2  24734  dchrptlem3  24735  dchrpt  24736  lgsval  24770  lgsval4lem  24777  lgsneg  24790  lgsmod  24792  rpvmasum2  24945  padicfval  25049  ostth2  25070  ostth3  25071  ostth  25072  lmif  25422  islmib  25424  wwlkn  26003  clwwlkn  26088  clwwlknprop  26093  htthlem  26951  htth  26952  pjhfval  27432  hosmval  27771  hommval  27772  hodmval  27773  hfsmval  27774  hfmmval  27775  brafval  27979  kbfval  27988  psgnfzto1st  28979  mdetpmtr1  29010  ordtcnvNEW  29087  ordtrest2NEW  29090  xrhval  29183  indval  29196  esum2dlem  29274  ofceq  29279  itgeq12dv  29508  ballotlemfval  29671  ptpcon  30262  cvmliftlem15  30327  cvmlift2lem4  30335  cvmlift2  30345  snmlval  30360  snmlflim  30361  mrsubfval  30452  mrsubrn  30457  elmsubrn  30472  msubrn  30473  msubco  30475  faclim  30678  faclim2  30680  trpredeq1  30757  trpredeq2  30758  knoppcnlem1  31446  knoppcnlem6  31451  knoppcnlem7  31452  csbrdgg  32134  curfv  32342  matunitlindflem2  32359  poimirlem5  32367  poimirlem6  32368  poimirlem7  32369  poimirlem8  32370  poimirlem10  32372  poimirlem11  32373  poimirlem12  32374  poimirlem15  32377  poimirlem16  32378  poimirlem17  32379  poimirlem18  32380  poimirlem19  32381  poimirlem20  32382  poimirlem21  32383  poimirlem22  32384  poimirlem27  32389  voliunnfl  32406  itg2addnclem  32414  itg2addnclem3  32416  itg2addnc  32417  itg2gt0cn  32418  iblabsnclem  32426  iblmulc2nc  32428  ftc1anclem2  32439  ftc1anclem6  32443  ftc1anclem8  32445  ftc1anc  32446  ftc2nc  32447  upixp  32477  rrncmslem  32584  ismrer1  32590  tendoplcbv  34864  tendopl  34865  tendoicbv  34882  tendoi  34883  dihfval  35321  lcfl7N  35591  lcfrlem8  35639  lcfrlem9  35640  lcf1o  35641  hvmapval  35850  hdmap1fval  35887  hdmapffval  35919  hdmapfval  35920  hgmapffval  35978  hgmapfval  35979  mzpclval  36089  mzpcl2  36094  mzpexpmpt  36109  mzpsubst  36112  mzpcompact2lem  36115  rmxfval  36269  rmyfval  36270  aomclem8  36432  hbtlem1  36495  hbtlem7  36497  itgpowd  36602  rfovfvd  37099  fsovrfovd  37106  fsovfvd  37107  fsovcnvlem  37110  dssmapfv2d  37115  dssmapnvod  37117  ntrneibex  37174  expgrowthi  37337  expgrowth  37339  binomcxplemdvsum  37359  addrval  37474  subrval  37475  mulvval  37476  fmulcl  38431  fmuldfeqlem1  38432  fprodcnlem  38449  fprodcn  38450  fnlimfv  38513  fnlimcnv  38517  fnlimfvre  38524  fnlimfvre2  38527  fnlimf  38528  fnlimabslt  38529  fprodcncf  38570  dvnmptdivc  38611  dvnxpaek  38615  dvnmul  38616  dvmptfprod  38618  dvnprodlem1  38619  dvnprodlem2  38620  dvnprodlem3  38621  dvnprod  38622  stoweidlem2  38678  stoweidlem17  38693  stoweidlem19  38695  stoweidlem20  38696  stoweidlem43  38719  stoweidlem62  38738  stoweid  38739  dirkercncflem2  38780  fourierdlem112  38894  fourierdlem113  38895  etransclem1  38911  etransclem5  38915  etransclem17  38927  etransclem19  38929  etransclem22  38932  sge0val  39042  ovnlecvr  39231  ovncvrrp  39237  ovn0lem  39238  ovnsubaddlem1  39243  ovnsubadd  39245  hsphoif  39249  hsphoival  39252  hoidmv1lelem1  39264  hoidmv1lelem2  39265  hoidmv1lelem3  39266  hoidmv1le  39267  hoidmvlelem1  39268  hoidmvlelem2  39269  hoidmvlelem3  39270  hoidmvlelem4  39271  hoidmvlelem5  39272  hoidmvle  39273  ovnhoilem1  39274  ovnhoi  39276  hoidifhspval  39281  ovncvr2  39284  hoidifhspval2  39288  hspmbllem2  39300  hspmbllem3  39301  hspmbl  39302  ovnovollem1  39329  vonioolem2  39355  vonioo  39356  vonicclem2  39358  vonicc  39359  smflimlem4  39443  smflim  39446  incistruhgr  40286  eucrct2eupth  41394  c0rhm  41683  c0rnghm  41684  lincop  41972  aacllem  42298
  Copyright terms: Public domain W3C validator