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

Theorem mpteq2dv 5148
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 484 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32mpteq2dva 5147 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  cmpt 5132
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ral 3138  df-opab 5115  df-mpt 5133
This theorem is referenced by:  ofeq  7405  mpocurryvald  7932  rdgeq1  8043  rdgeq2  8044  omv  8133  oev  8135  oieq1  8973  oieq2  8974  cantnflem1  9149  wunex2  10158  wuncval2  10167  rpnnen1  12379  seqof2  13433  relexpsucnnr  14384  relexp1g  14385  limsupval  14831  sumeq2w  15049  sumeq2ii  15050  cbvsum  15052  summo  15074  fsum  15077  fsumrlim  15166  fsumo1  15167  prodeq2w  15266  prodmo  15290  fprod  15295  bpolylem  15402  rpnnen2lem1  15567  rpnnen2lem2  15568  1arithlem1  16257  vdwapval  16307  vdwlem6  16320  vdwlem8  16322  vdwlem9  16323  vdwlem10  16324  ramub1lem2  16361  ramcl  16363  sloteq  16488  prdsplusgval  16746  prdsmulrval  16748  prdsdsval  16751  prdsvscaval  16752  ismon  17003  fucco  17232  curf1  17475  curf2  17479  yonedalem4a  17525  smndex1gbas  18067  smndex1gid  18068  grplactfval  18200  galactghm  18532  pmtrval  18579  sylow1  18728  sylow2b  18748  sylow3lem5  18756  sylow3  18758  iscyg  18998  gsumzaddlem  19041  gsumzmhm  19057  ablfac2  19211  gsumdixp  19362  fczpsrbag  20147  psrmulfval  20165  mvrval  20201  subrgmvr  20242  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  mplmon2  20273  subrgascl  20278  evlslem2  20292  evlslem3  20293  evlslem1  20295  mpfrcl  20298  evlsval  20299  evlsvar  20303  mpfind  20320  selvfval  20330  selvval  20331  mhpfval  20332  coe1fval  20373  pf1ind  20518  evl1gsumadd  20521  zncyg  20695  phllmhm  20776  isphld  20798  frlmgsum  20916  frlmipval  20923  frlmphl  20925  uvcval  20929  mamuval  20997  mamufv  20998  matgsum  21046  madetsumid  21070  mat1dimmul  21085  mvmulval  21152  mvmulfv  21153  mavmulfv  21155  1mavmul  21157  marepvval0  21175  mulmarep1gsum1  21182  mdetleib  21196  mdetleib2  21197  mdetfval1  21199  mdetleib1  21200  mdet0pr  21201  m1detdiag  21206  mdetralt  21217  mdetunilem9  21229  m2detleib  21240  smadiadetlem3  21277  mat2pmatmul  21339  decpmatmul  21380  decpmatmulsumfsupp  21381  pmatcollpw1  21384  monmatcollpw  21387  pmatcollpw3lem  21391  pmatcollpw3fi1lem2  21395  pm2mpval  21403  pm2mpfval  21404  mply1topmatval  21412  mp2pm2mplem1  21414  mp2pm2mplem3  21416  ptbasfi  22189  ptcnplem  22229  ptrescn  22247  cnmpt2k  22296  xkohmeo  22423  fmval  22551  fmf  22553  ptcmpg  22665  tmdmulg  22700  prdstmdd  22732  tsmspropd  22740  prdsxmslem2  23139  metdsval  23455  fsumcn  23478  expcn  23480  lebnumlem3  23571  pcoval  23619  pi1xfrcnv  23665  cphsscph  23858  rrxds  24000  rrxmval  24012  itg11  24298  mbfi1fseqlem2  24323  mbfi1fseqlem6  24327  mbfi1fseq  24328  mbfi1flimlem  24329  mbfmullem  24332  itg2const  24347  itg2mulc  24354  itg2monolem1  24357  itg2i1fseqle  24361  itg2i1fseq  24362  itg2addlem  24365  itg2cnlem1  24368  itg2cn  24370  isibl  24372  isibl2  24373  iblitg  24375  itgz  24387  itgvallem  24391  itgvallem3  24392  iblcnlem1  24394  itgcnlem  24396  iblrelem  24397  iblposlem  24398  iblpos  24399  itgrevallem1  24401  itgposval  24402  iblss2  24412  itgss  24418  itgfsum  24433  iblabslem  24434  iblmulc2  24437  bddmulibl  24445  itgcn  24451  ellimc  24479  dvnfval  24528  cpnfval  24538  dvexp  24559  dvexp2  24560  dvmptfsum  24581  dvlipcn  24600  dvivthlem1  24614  dvfsumle  24627  dvfsumabs  24629  dvfsumlem2  24633  itgpowd  24656  elply2  24796  elplyr  24801  elplyd  24802  coeeu  24825  coelem  24826  coeeq  24827  plyco  24841  coe11  24853  coe1termlem  24858  dgrcolem1  24873  dvply2g  24884  elqaalem3  24920  eltayl  24958  tayl0  24960  taylthlem1  24971  taylthlem2  24972  ulmcau  24993  ulmdvlem1  24998  ulmdvlem3  25000  mtest  25002  mtestbdd  25003  pserval  25008  pserulm  25020  psercn  25024  pserdvlem2  25026  abelthlem3  25031  logtayl  25254  dvcxp1  25332  dvcncxp1  25335  logbmpt  25377  dmarea  25546  lgamgulmlem2  25618  lgamgulmlem5  25621  musum  25779  dchrptlem2  25852  dchrptlem3  25853  dchrpt  25854  lgsval  25888  lgsval4lem  25895  lgsneg  25908  lgsmod  25910  rpvmasum2  26099  padicfval  26203  ostth2  26224  ostth3  26225  ostth  26226  lmif  26582  islmib  26584  incistruhgr  26875  eucrct2eupth  28033  htthlem  28703  htth  28704  pjhfval  29182  hosmval  29521  hommval  29522  hodmval  29523  hfsmval  29524  hfmmval  29525  brafval  29729  kbfval  29738  mptprop  30445  psgnfzto1st  30779  linds2eq  30977  lbsdiflsp0  31082  fedgmullem1  31085  fedgmullem2  31086  fedgmul  31087  mdetpmtr1  31148  ordtcnvNEW  31220  ordtrest2NEW  31223  xrhval  31316  indval  31329  esum2dlem  31408  ofceq  31413  itgeq12dv  31641  ballotlemfval  31804  vtsval  31965  lpadval  32004  ptpconn  32537  cvmliftlem15  32602  cvmlift2lem4  32610  cvmlift2  32620  snmlval  32635  snmlflim  32636  satf  32657  mrsubfval  32812  mrsubrn  32817  elmsubrn  32832  msubrn  32833  msubco  32835  faclim  33035  faclim2  33037  trpredeq1  33116  trpredeq2  33117  knoppcnlem1  33889  knoppcnlem6  33894  knoppcnlem7  33895  bj-evaleq  34431  csbrdgg  34691  curfv  34982  matunitlindflem2  34999  poimirlem5  35007  poimirlem6  35008  poimirlem7  35009  poimirlem8  35010  poimirlem10  35012  poimirlem11  35013  poimirlem12  35014  poimirlem15  35017  poimirlem16  35018  poimirlem17  35019  poimirlem18  35020  poimirlem19  35021  poimirlem20  35022  poimirlem21  35023  poimirlem22  35024  poimirlem27  35029  voliunnfl  35046  itg2addnclem  35053  itg2addnclem3  35055  itg2addnc  35056  itg2gt0cn  35057  iblabsnclem  35065  iblmulc2nc  35067  ftc1anclem2  35076  ftc1anclem6  35080  ftc1anclem8  35082  ftc1anc  35083  ftc2nc  35084  upixp  35112  rrncmslem  35215  ismrer1  35221  tendoplcbv  38016  tendopl  38017  tendoicbv  38034  tendoi  38035  dihfval  38472  lcfl7N  38742  lcfrlem8  38790  lcfrlem9  38791  lcf1o  38792  hvmapval  39001  hdmap1fval  39037  hdmapffval  39067  hdmapfval  39068  hgmapffval  39126  hgmapfval  39127  lcmineqlem7  39271  lcmineqlem12  39276  mzpclval  39582  mzpcl2  39587  mzpexpmpt  39602  mzpsubst  39605  mzpcompact2lem  39608  rmxfval  39761  rmyfval  39762  aomclem8  39921  hbtlem1  39983  hbtlem7  39985  rfovfvd  40620  fsovrfovd  40627  fsovfvd  40628  fsovcnvlem  40631  dssmapfv2d  40636  dssmapnvod  40638  ntrneibex  40695  mnringmulrvald  40855  mnringmulrcld  40856  expgrowthi  40957  expgrowth  40959  binomcxplemdvsum  40979  addrval  41090  subrval  41091  mulvval  41092  fmulcl  42149  fmuldfeqlem1  42150  fprodcnlem  42167  fprodcn  42168  fnlimfv  42231  fnlimcnv  42235  fnlimfvre  42242  fnlimfvre2  42245  fnlimf  42246  fnlimabslt  42247  liminfval  42327  limsupresxr  42334  liminfresxr  42335  liminfvalxr  42351  fprodcncf  42468  dvnmptdivc  42506  dvnxpaek  42510  dvnmul  42511  dvmptfprod  42513  dvnprodlem1  42514  dvnprodlem2  42515  dvnprodlem3  42516  dvnprod  42517  stoweidlem2  42570  stoweidlem17  42585  stoweidlem19  42587  stoweidlem20  42588  stoweidlem43  42611  stoweidlem62  42630  stoweid  42631  dirkercncflem2  42672  fourierdlem112  42786  fourierdlem113  42787  etransclem1  42803  etransclem5  42807  etransclem17  42819  etransclem19  42821  etransclem22  42824  sge0val  42931  ovnlecvr  43123  ovncvrrp  43129  ovn0lem  43130  ovnsubaddlem1  43135  ovnsubadd  43137  hsphoif  43141  hsphoival  43144  hoidmv1lelem1  43156  hoidmv1lelem2  43157  hoidmv1lelem3  43158  hoidmv1le  43159  hoidmvlelem1  43160  hoidmvlelem2  43161  hoidmvlelem3  43162  hoidmvlelem4  43163  hoidmvlelem5  43164  hoidmvle  43165  ovnhoilem1  43166  ovnhoi  43168  hoidifhspval  43173  ovncvr2  43176  hoidifhspval2  43180  hspmbllem2  43192  hspmbllem3  43193  hspmbl  43194  ovnovollem1  43221  vonioolem2  43246  vonioo  43247  vonicclem2  43249  vonicc  43250  smflimlem4  43333  smflim  43336  smflim2  43363  smfsuplem2  43369  smfsup  43371  smfinf  43375  smflimsuplem2  43378  smflimsuplem5  43381  smflimsuplem7  43383  smflimsup  43385  c0rhm  44462  c0rnghm  44463  lincop  44743  1arymaptfv  44980  itcoval  45001  itcovalpc  45012  itcovalt2  45017  ackvalsuc1mpt  45018  ackval1  45021  aacllem  45255
  Copyright terms: Public domain W3C validator