Theorem mpteq2dv 5186

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

Step	Hyp	Ref	Expression
1		mpteq2dv.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5185	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5155  df-mpt 5174

This theorem is referenced by:  ifmpt2v  7451  ofeqd  7615  mpocurryvald  8203  rdgeq1  8333  rdgeq2  8334  omv  8430  oev  8432  oieq1  9404  oieq2  9405  cantnflem1  9585  wunex2  10632  wuncval2  10641  rpnnen1  12884  seqof2  13967  relexpsucnnr  14932  relexp1g  14933  limsupval  15381  sumeq2w  15599  sumeq2ii  15600  cbvsum  15602  cbvsumv  15603  sumeq2sdv  15610  summo  15624  fsum  15627  fsumrlim  15718  fsumo1  15719  prodeq1  15814  prodeq2w  15817  prodeq2sdv  15830  prodmo  15843  fprod  15848  bpolylem  15955  rpnnen2lem1  16123  rpnnen2lem2  16124  1arithlem1  16835  vdwapval  16885  vdwlem6  16898  vdwlem8  16900  vdwlem9  16901  vdwlem10  16902  ramub1lem2  16939  ramcl  16941  sloteq  17094  prdsplusgval  17377  prdsmulrval  17379  prdsdsval  17382  prdsvscaval  17383  ismon  17640  fucco  17872  curf1  18131  curf2  18135  yonedalem4a  18181  smndex1gbas  18776  smndex1gid  18777  grplactfval  18920  galactghm  19283  pmtrval  19330  sylow1  19482  sylow2b  19502  sylow3lem5  19510  sylow3  19512  iscyg  19758  gsumzaddlem  19800  gsumzmhm  19816  ablfac2  19970  gsumdixp  20204  c0rhm  20419  c0rnghm  20420  zncyg  21455  phllmhm  21539  isphld  21561  frlmgsum  21679  frlmipval  21686  frlmphl  21688  uvcval  21692  fczpsrbag  21828  psrmulfval  21850  psrascl  21886  mvrval  21889  subrgmvr  21938  mplcoe1  21942  mplcoe3  21943  mplcoe5  21945  mplmon2  21966  subrgascl  21971  evlslem2  21984  evlslem3  21985  evlslem1  21987  mpfrcl  21990  evlsval  21991  evlsvar  21995  mpfind  22012  selvfval  22019  selvval  22020  mhpfval  22023  psdfval  22043  psdval  22044  psdmvr  22054  coe1fval  22088  pf1ind  22240  evl1gsumadd  22243  rhmmpl  22268  rhmply1vr1  22272  mamuval  22278  mamufv  22279  matgsum  22322  madetsumid  22346  mat1dimmul  22361  mvmulval  22428  mvmulfv  22429  mavmulfv  22431  1mavmul  22433  marepvval0  22451  mulmarep1gsum1  22458  mdetleib  22472  mdetleib2  22473  mdetfval1  22475  mdetleib1  22476  mdet0pr  22477  m1detdiag  22482  mdetralt  22493  mdetunilem9  22505  m2detleib  22516  smadiadetlem3  22553  mat2pmatmul  22616  decpmatmul  22657  decpmatmulsumfsupp  22658  pmatcollpw1  22661  monmatcollpw  22664  pmatcollpw3lem  22668  pmatcollpw3fi1lem2  22672  pm2mpval  22680  pm2mpfval  22681  mply1topmatval  22689  mp2pm2mplem1  22691  mp2pm2mplem3  22693  ptbasfi  23466  ptcnplem  23506  ptrescn  23524  cnmpt2k  23573  xkohmeo  23700  fmval  23828  fmf  23830  ptcmpg  23942  tmdmulg  23977  prdstmdd  24009  tsmspropd  24017  prdsxmslem2  24415  metdsval  24734  fsumcn  24759  expcn  24761  expcnOLD  24763  lebnumlem3  24860  pcoval  24909  pi1xfrcnv  24955  cphsscph  25149  rrxds  25291  rrxmval  25303  itg11  25590  mbfi1fseqlem2  25615  mbfi1fseqlem6  25619  mbfi1fseq  25620  mbfi1flimlem  25621  mbfmullem  25624  itg2const  25639  itg2mulc  25646  itg2monolem1  25649  itg2i1fseqle  25653  itg2i1fseq  25654  itg2addlem  25657  itg2cnlem1  25660  itg2cn  25662  isibl  25664  isibl2  25665  iblitg  25667  itgeq1  25672  itgz  25680  itgvallem  25684  itgvallem3  25685  iblcnlem1  25687  itgcnlem  25689  iblrelem  25690  iblposlem  25691  iblpos  25692  itgrevallem1  25694  itgposval  25695  iblss2  25705  itgss  25711  itgfsum  25726  iblabslem  25727  iblmulc2  25730  bddmulibl  25738  itgcn  25744  ellimc  25772  dvnfval  25822  cpnfval  25832  dvexp  25855  dvexp2  25856  dvmptfsum  25877  dvlipcn  25897  dvivthlem1  25911  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumlem2  25931  dvfsumlem2OLD  25932  itgpowd  25955  elply2  26099  elplyr  26104  elplyd  26105  coeeu  26128  coelem  26129  coeeq  26130  plyco  26144  coe11  26156  coe1termlem  26161  dgrcolem1  26177  dvply2g  26190  dvply2gOLD  26191  elqaalem3  26227  eltayl  26265  tayl0  26267  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmcau  26302  ulmdvlem1  26307  ulmdvlem3  26309  mtest  26311  mtestbdd  26312  pserval  26317  pserulm  26329  psercn  26334  pserdvlem2  26336  abelthlem3  26341  logtayl  26567  dvcxp1  26647  dvcncxp1  26650  logbmpt  26696  dmarea  26865  lgamgulmlem2  26938  lgamgulmlem5  26941  musum  27099  dchrptlem2  27174  dchrptlem3  27175  dchrpt  27176  lgsval  27210  lgsval4lem  27217  lgsneg  27230  lgsmod  27232  rpvmasum2  27421  padicfval  27525  ostth2  27546  ostth3  27547  ostth  27548  lmif  28730  islmib  28732  incistruhgr  29024  eucrct2eupth  30189  htthlem  30861  htth  30862  pjhfval  31340  hosmval  31679  hommval  31680  hodmval  31681  hfsmval  31682  hfmmval  31683  brafval  31887  kbfval  31896  mptprop  32641  indval  32797  psgnfzto1st  33048  fxpsubm  33115  fxpsubg  33116  fxpsubrg  33117  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspn  33187  elrgspnsubrunlem1  33188  linds2eq  33319  elrspunidl  33366  elrspunsn  33367  evl1deg1  33512  evl1deg2  33513  evl1deg3  33514  mplvrpmfgalem  33547  mplvrpmga  33548  mplvrpmmhm  33549  lbsdiflsp0  33599  fedgmullem1  33602  fedgmullem2  33603  fedgmul  33604  evls1fldgencl  33643  fldextrspunlsplem  33646  fldextrspunlsp  33647  extdgfialglem2  33666  mdetpmtr1  33796  zar0ring  33851  ordtcnvNEW  33893  ordtrest2NEW  33896  xrhval  33991  esum2dlem  34065  ofceq  34070  itgeq12dv  34300  ballotlemfval  34464  vtsval  34611  lpadval  34650  ptpconn  35216  cvmliftlem15  35281  cvmlift2lem4  35289  cvmlift2  35299  snmlval  35314  snmlflim  35315  satf  35336  mrsubfval  35491  mrsubrn  35496  elmsubrn  35511  msubrn  35512  msubco  35514  faclim  35729  faclim2  35731  prodeq12sdv  36202  itgeq12sdv  36203  cbvsumdavw  36263  cbvproddavw  36264  cbvsumdavw2  36279  cbvproddavw2  36280  knoppcnlem1  36477  knoppcnlem6  36482  knoppcnlem7  36483  bj-evaleq  37056  csbrdgg  37313  curfv  37590  matunitlindflem2  37607  poimirlem5  37615  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem10  37620  poimirlem11  37621  poimirlem12  37622  poimirlem15  37625  poimirlem16  37626  poimirlem17  37627  poimirlem18  37628  poimirlem19  37629  poimirlem20  37630  poimirlem21  37631  poimirlem22  37632  poimirlem27  37637  voliunnfl  37654  itg2addnclem  37661  itg2addnclem3  37663  itg2addnc  37664  itg2gt0cn  37665  iblabsnclem  37673  iblmulc2nc  37675  ftc1anclem2  37684  ftc1anclem6  37688  ftc1anclem8  37690  ftc1anc  37691  ftc2nc  37692  upixp  37719  rrncmslem  37822  ismrer1  37828  tendoplcbv  40764  tendopl  40765  tendoicbv  40782  tendoi  40783  dihfval  41220  lcfl7N  41490  lcfrlem8  41538  lcfrlem9  41539  lcf1o  41540  hvmapval  41749  hdmap1fval  41785  hdmapffval  41815  hdmapfval  41816  hgmapffval  41874  hgmapfval  41875  lcmineqlem7  42018  lcmineqlem12  42023  aks6d1c6lem5  42160  rhmpsr  42535  evlsvval  42543  evlsvvval  42546  evlsbagval  42549  selvvvval  42568  evlselv  42570  fsuppind  42573  fsuppssindlem2  42575  fsuppssind  42576  mzpclval  42708  mzpcl2  42713  mzpexpmpt  42728  mzpsubst  42731  mzpcompact2lem  42734  rmxfval  42887  rmyfval  42888  aomclem8  43044  hbtlem1  43106  hbtlem7  43108  rfovfvd  43985  fsovrfovd  43992  fsovfvd  43993  fsovcnvlem  43996  dssmapfv2d  44001  dssmapnvod  44003  ntrneibex  44056  mnringmulrvald  44210  mnringmulrcld  44211  expgrowthi  44316  expgrowth  44318  binomcxplemdvsum  44338  addrval  44449  subrval  44450  mulvval  44451  fmulcl  45572  fmuldfeqlem1  45573  fprodcnlem  45590  fprodcn  45591  fnlimfv  45654  fnlimcnv  45658  fnlimfvre  45665  fnlimfvre2  45668  fnlimf  45669  fnlimabslt  45670  liminfval  45750  limsupresxr  45757  liminfresxr  45758  liminfvalxr  45774  fprodcncf  45891  dvnmptdivc  45929  dvnxpaek  45933  dvnmul  45934  dvmptfprod  45936  dvnprodlem1  45937  dvnprodlem2  45938  dvnprodlem3  45939  dvnprod  45940  stoweidlem2  45993  stoweidlem17  46008  stoweidlem19  46010  stoweidlem20  46011  stoweidlem43  46034  stoweidlem62  46053  stoweid  46054  dirkercncflem2  46095  fourierdlem112  46209  fourierdlem113  46210  etransclem1  46226  etransclem5  46230  etransclem17  46242  etransclem19  46244  etransclem22  46247  sge0val  46357  ovnlecvr  46549  ovncvrrp  46555  ovn0lem  46556  ovnsubaddlem1  46561  ovnsubadd  46563  hsphoif  46567  hsphoival  46570  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmv1le  46585  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem4  46589  hoidmvlelem5  46590  hoidmvle  46591  ovnhoilem1  46592  ovnhoi  46594  hoidifhspval  46599  ovncvr2  46602  hoidifhspval2  46606  hspmbllem2  46618  hspmbllem3  46619  hspmbl  46620  ovnovollem1  46647  vonioolem2  46672  vonioo  46673  vonicclem2  46675  vonicc  46676  smflimlem4  46765  smflim  46768  smflim2  46797  smfsuplem2  46803  smfsup  46805  smfinf  46809  smflimsuplem2  46812  smflimsuplem5  46815  smflimsuplem7  46817  smflimsup  46819  cfsetsnfsetfo  47054  lincop  48403  1arymaptfv  48635  itcoval  48656  itcovalpc  48667  itcovalt2  48672  ackvalsuc1mpt  48673  ackval1  48676  fuco21  49331  prcofval  49373  aacllem  49796