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

Theorem mpteq2dv 4897
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 472 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32mpteq2dva 4896 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  cmpt 4881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ral 3055  df-opab 4865  df-mpt 4882
This theorem is referenced by:  ofeq  7065  mpt2curryvald  7566  rdgeq1  7677  rdgeq2  7678  omv  7763  oev  7765  oieq1  8584  oieq2  8585  cantnflem1  8761  wunex2  9772  wuncval2  9781  rpnnen1  12033  seqof2  13073  relexpsucnnr  13984  relexp1g  13985  limsupval  14424  sumeq2w  14641  sumeq2ii  14642  cbvsum  14644  summo  14667  fsum  14670  fsumrlim  14762  fsumo1  14763  prodeq2w  14861  prodmo  14885  fprod  14890  bpolylem  14998  rpnnen2lem1  15162  rpnnen2lem2  15163  1arithlem1  15849  vdwapval  15899  vdwlem6  15912  vdwlem8  15914  vdwlem9  15915  vdwlem10  15916  ramub1lem2  15953  ramcl  15955  sloteq  16084  prdsplusgval  16355  prdsmulrval  16357  prdsdsval  16360  prdsvscaval  16361  ismon  16614  fucco  16843  curf1  17086  curf2  17090  yonedalem4a  17136  grplactfval  17737  galactghm  18043  pmtrval  18091  sylow1  18238  sylow2b  18258  sylow3lem5  18266  sylow3  18268  iscyg  18501  gsumzaddlem  18541  gsumzmhm  18557  ablfac2  18708  gsumdixp  18829  fczpsrbag  19589  psrmulfval  19607  mvrval  19643  subrgmvr  19683  mplcoe1  19687  mplcoe3  19688  mplcoe5  19690  mplmon2  19715  subrgascl  19720  evlslem2  19734  evlslem3  19736  evlslem1  19737  mpfrcl  19740  evlsval  19741  evlsvar  19745  mpfind  19758  coe1fval  19797  pf1ind  19941  evl1gsumadd  19944  zncyg  20119  phllmhm  20199  isphld  20221  frlmgsum  20333  frlmipval  20340  frlmphl  20342  uvcval  20346  mamuval  20414  mamufv  20415  matgsum  20465  madetsumid  20489  mat1dimmul  20504  mvmulval  20571  mvmulfv  20572  mavmulfv  20574  1mavmul  20576  marepvval0  20594  mulmarep1gsum1  20601  mdetleib  20615  mdetleib2  20616  mdetfval1  20618  mdetleib1  20619  mdet0pr  20620  m1detdiag  20625  mdetralt  20636  mdetunilem9  20648  m2detleib  20659  smadiadetlem3  20696  mat2pmatmul  20758  decpmatmul  20799  decpmatmulsumfsupp  20800  pmatcollpw1  20803  monmatcollpw  20806  pmatcollpw3lem  20810  pmatcollpw3fi1lem2  20814  pm2mpval  20822  pm2mpfval  20823  mply1topmatval  20831  mp2pm2mplem1  20833  mp2pm2mplem3  20835  ptbasfi  21606  ptcnplem  21646  ptrescn  21664  cnmpt2k  21713  xkohmeo  21840  fmval  21968  fmf  21970  ptcmpg  22082  tmdmulg  22117  prdstmdd  22148  tsmspropd  22156  prdsxmslem2  22555  metdsval  22871  fsumcn  22894  expcn  22896  lebnumlem3  22983  pcoval  23031  pi1xfrcnv  23077  rrxds  23401  rrxmval  23408  itg11  23677  mbfi1fseqlem2  23702  mbfi1fseqlem6  23706  mbfi1fseq  23707  mbfi1flimlem  23708  mbfmullem  23711  itg2const  23726  itg2mulc  23733  itg2monolem1  23736  itg2i1fseqle  23740  itg2i1fseq  23741  itg2addlem  23744  itg2cnlem1  23747  itg2cn  23749  isibl  23751  isibl2  23752  iblitg  23754  itgz  23766  itgvallem  23770  itgvallem3  23771  iblcnlem1  23773  itgcnlem  23775  iblrelem  23776  iblposlem  23777  iblpos  23778  itgrevallem1  23780  itgposval  23781  iblss2  23791  itgss  23797  itgfsum  23812  iblabslem  23813  iblmulc2  23816  bddmulibl  23824  itgcn  23828  ellimc  23856  dvnfval  23904  cpnfval  23914  dvexp  23935  dvexp2  23936  dvmptfsum  23957  dvlipcn  23976  dvivthlem1  23990  dvfsumle  24003  dvfsumabs  24005  dvfsumlem2  24009  elply2  24171  elplyr  24176  elplyd  24177  coeeu  24200  coelem  24201  coeeq  24202  plyco  24216  coe11  24228  coe1termlem  24233  dgrcolem1  24248  dvply2g  24259  elqaalem3  24295  eltayl  24333  tayl0  24335  taylthlem1  24346  taylthlem2  24347  ulmcau  24368  ulmdvlem1  24373  ulmdvlem3  24375  mtest  24377  mtestbdd  24378  pserval  24383  pserulm  24395  psercn  24399  pserdvlem2  24401  abelthlem3  24406  logtayl  24626  dvcxp1  24701  dvcncxp1  24704  logbmpt  24746  dmarea  24904  lgamgulmlem2  24976  lgamgulmlem5  24979  musum  25137  dchrptlem2  25210  dchrptlem3  25211  dchrpt  25212  lgsval  25246  lgsval4lem  25253  lgsneg  25266  lgsmod  25268  rpvmasum2  25421  padicfval  25525  ostth2  25546  ostth3  25547  ostth  25548  lmif  25897  islmib  25899  incistruhgr  26194  eucrct2eupth  27418  htthlem  28104  htth  28105  pjhfval  28585  hosmval  28924  hommval  28925  hodmval  28926  hfsmval  28927  hfmmval  28928  brafval  29132  kbfval  29141  psgnfzto1st  30185  mdetpmtr1  30219  ordtcnvNEW  30296  ordtrest2NEW  30299  xrhval  30392  indval  30405  esum2dlem  30484  ofceq  30489  itgeq12dv  30718  ballotlemfval  30881  vtsval  31045  ptpconn  31543  cvmliftlem15  31608  cvmlift2lem4  31616  cvmlift2  31626  snmlval  31641  snmlflim  31642  mrsubfval  31733  mrsubrn  31738  elmsubrn  31753  msubrn  31754  msubco  31756  faclim  31960  faclim2  31962  trpredeq1  32046  trpredeq2  32047  knoppcnlem1  32810  knoppcnlem6  32815  knoppcnlem7  32816  bj-evaleq  33348  csbrdgg  33504  curfv  33720  matunitlindflem2  33737  poimirlem5  33745  poimirlem6  33746  poimirlem7  33747  poimirlem8  33748  poimirlem10  33750  poimirlem11  33751  poimirlem12  33752  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem18  33758  poimirlem19  33759  poimirlem20  33760  poimirlem21  33761  poimirlem22  33762  poimirlem27  33767  voliunnfl  33784  itg2addnclem  33792  itg2addnclem3  33794  itg2addnc  33795  itg2gt0cn  33796  iblabsnclem  33804  iblmulc2nc  33806  ftc1anclem2  33817  ftc1anclem6  33821  ftc1anclem8  33823  ftc1anc  33824  ftc2nc  33825  upixp  33855  rrncmslem  33962  ismrer1  33968  tendoplcbv  36583  tendopl  36584  tendoicbv  36601  tendoi  36602  dihfval  37040  lcfl7N  37310  lcfrlem8  37358  lcfrlem9  37359  lcf1o  37360  hvmapval  37569  hdmap1fval  37606  hdmapffval  37638  hdmapfval  37639  hgmapffval  37697  hgmapfval  37698  mzpclval  37808  mzpcl2  37813  mzpexpmpt  37828  mzpsubst  37831  mzpcompact2lem  37834  rmxfval  37988  rmyfval  37989  aomclem8  38151  hbtlem1  38213  hbtlem7  38215  itgpowd  38320  rfovfvd  38816  fsovrfovd  38823  fsovfvd  38824  fsovcnvlem  38827  dssmapfv2d  38832  dssmapnvod  38834  ntrneibex  38891  expgrowthi  39052  expgrowth  39054  binomcxplemdvsum  39074  addrval  39190  subrval  39191  mulvval  39192  fmulcl  40334  fmuldfeqlem1  40335  fprodcnlem  40352  fprodcn  40353  fnlimfv  40416  fnlimcnv  40420  fnlimfvre  40427  fnlimfvre2  40430  fnlimf  40431  fnlimabslt  40432  liminfval  40512  limsupresxr  40519  liminfresxr  40520  liminfvalxr  40536  fprodcncf  40635  dvnmptdivc  40674  dvnxpaek  40678  dvnmul  40679  dvmptfprod  40681  dvnprodlem1  40682  dvnprodlem2  40683  dvnprodlem3  40684  dvnprod  40685  stoweidlem2  40740  stoweidlem17  40755  stoweidlem19  40757  stoweidlem20  40758  stoweidlem43  40781  stoweidlem62  40800  stoweid  40801  dirkercncflem2  40842  fourierdlem112  40956  fourierdlem113  40957  etransclem1  40973  etransclem5  40977  etransclem17  40989  etransclem19  40991  etransclem22  40994  sge0val  41104  ovnlecvr  41296  ovncvrrp  41302  ovn0lem  41303  ovnsubaddlem1  41308  ovnsubadd  41310  hsphoif  41314  hsphoival  41317  hoidmv1lelem1  41329  hoidmv1lelem2  41330  hoidmv1lelem3  41331  hoidmv1le  41332  hoidmvlelem1  41333  hoidmvlelem2  41334  hoidmvlelem3  41335  hoidmvlelem4  41336  hoidmvlelem5  41337  hoidmvle  41338  ovnhoilem1  41339  ovnhoi  41341  hoidifhspval  41346  ovncvr2  41349  hoidifhspval2  41353  hspmbllem2  41365  hspmbllem3  41366  hspmbl  41367  ovnovollem1  41394  vonioolem2  41419  vonioo  41420  vonicclem2  41422  vonicc  41423  smflimlem4  41506  smflim  41509  smflim2  41536  smfsuplem2  41542  smfsup  41544  smfinf  41548  smflimsuplem2  41551  smflimsuplem5  41554  smflimsuplem7  41556  smflimsup  41558  c0rhm  42440  c0rnghm  42441  lincop  42725  aacllem  43078
  Copyright terms: Public domain W3C validator