Theorem mpteq2dv 5185

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 5184	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ↦ cmpt 5172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5154  df-mpt 5173

This theorem is referenced by:  ifmpt2v  7448  ofeqd  7612  mpocurryvald  8200  rdgeq1  8330  rdgeq2  8331  omv  8427  oev  8429  oieq1  9398  oieq2  9399  cantnflem1  9579  wunex2  10629  wuncval2  10638  rpnnen1  12881  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  18810  smndex1gid  18811  grplactfval  18954  galactghm  19317  pmtrval  19364  sylow1  19516  sylow2b  19536  sylow3lem5  19544  sylow3  19546  iscyg  19792  gsumzaddlem  19834  gsumzmhm  19850  ablfac2  20004  gsumdixp  20238  c0rhm  20450  c0rnghm  20451  zncyg  21486  phllmhm  21570  isphld  21592  frlmgsum  21710  frlmipval  21717  frlmphl  21719  uvcval  21723  fczpsrbag  21859  psrmulfval  21881  psrascl  21917  mvrval  21920  subrgmvr  21969  mplcoe1  21973  mplcoe3  21974  mplcoe5  21976  mplmon2  21997  subrgascl  22002  evlslem2  22015  evlslem3  22016  evlslem1  22018  mpfrcl  22021  evlsval  22022  evlsvar  22026  mpfind  22043  selvfval  22050  selvval  22051  mhpfval  22054  psdfval  22074  psdval  22075  psdmvr  22085  coe1fval  22119  pf1ind  22271  evl1gsumadd  22274  rhmmpl  22299  rhmply1vr1  22303  mamuval  22309  mamufv  22310  matgsum  22353  madetsumid  22377  mat1dimmul  22392  mvmulval  22459  mvmulfv  22460  mavmulfv  22462  1mavmul  22464  marepvval0  22482  mulmarep1gsum1  22489  mdetleib  22503  mdetleib2  22504  mdetfval1  22506  mdetleib1  22507  mdet0pr  22508  m1detdiag  22513  mdetralt  22524  mdetunilem9  22536  m2detleib  22547  smadiadetlem3  22584  mat2pmatmul  22647  decpmatmul  22688  decpmatmulsumfsupp  22689  pmatcollpw1  22692  monmatcollpw  22695  pmatcollpw3lem  22699  pmatcollpw3fi1lem2  22703  pm2mpval  22711  pm2mpfval  22712  mply1topmatval  22720  mp2pm2mplem1  22722  mp2pm2mplem3  22724  ptbasfi  23497  ptcnplem  23537  ptrescn  23555  cnmpt2k  23604  xkohmeo  23731  fmval  23859  fmf  23861  ptcmpg  23973  tmdmulg  24008  prdstmdd  24040  tsmspropd  24048  prdsxmslem2  24445  metdsval  24764  fsumcn  24789  expcn  24791  expcnOLD  24793  lebnumlem3  24890  pcoval  24939  pi1xfrcnv  24985  cphsscph  25179  rrxds  25321  rrxmval  25333  itg11  25620  mbfi1fseqlem2  25645  mbfi1fseqlem6  25649  mbfi1fseq  25650  mbfi1flimlem  25651  mbfmullem  25654  itg2const  25669  itg2mulc  25676  itg2monolem1  25679  itg2i1fseqle  25683  itg2i1fseq  25684  itg2addlem  25687  itg2cnlem1  25690  itg2cn  25692  isibl  25694  isibl2  25695  iblitg  25697  itgeq1  25702  itgz  25710  itgvallem  25714  itgvallem3  25715  iblcnlem1  25717  itgcnlem  25719  iblrelem  25720  iblposlem  25721  iblpos  25722  itgrevallem1  25724  itgposval  25725  iblss2  25735  itgss  25741  itgfsum  25756  iblabslem  25757  iblmulc2  25760  bddmulibl  25768  itgcn  25774  ellimc  25802  dvnfval  25852  cpnfval  25862  dvexp  25885  dvexp2  25886  dvmptfsum  25907  dvlipcn  25927  dvivthlem1  25941  dvfsumle  25954  dvfsumleOLD  25955  dvfsumabs  25957  dvfsumlem2  25961  dvfsumlem2OLD  25962  itgpowd  25985  elply2  26129  elplyr  26134  elplyd  26135  coeeu  26158  coelem  26159  coeeq  26160  plyco  26174  coe11  26186  coe1termlem  26191  dgrcolem1  26207  dvply2g  26220  dvply2gOLD  26221  elqaalem3  26257  eltayl  26295  tayl0  26297  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  ulmcau  26332  ulmdvlem1  26337  ulmdvlem3  26339  mtest  26341  mtestbdd  26342  pserval  26347  pserulm  26359  psercn  26364  pserdvlem2  26366  abelthlem3  26371  logtayl  26597  dvcxp1  26677  dvcncxp1  26680  logbmpt  26726  dmarea  26895  lgamgulmlem2  26968  lgamgulmlem5  26971  musum  27129  dchrptlem2  27204  dchrptlem3  27205  dchrpt  27206  lgsval  27240  lgsval4lem  27247  lgsneg  27260  lgsmod  27262  rpvmasum2  27451  padicfval  27555  ostth2  27576  ostth3  27577  ostth  27578  lmif  28764  islmib  28766  incistruhgr  29058  eucrct2eupth  30223  htthlem  30895  htth  30896  pjhfval  31374  hosmval  31713  hommval  31714  hodmval  31715  hfsmval  31716  hfmmval  31717  brafval  31921  kbfval  31930  mptprop  32677  indval  32832  psgnfzto1st  33072  fxpsubm  33139  fxpsubg  33140  fxpsubrg  33141  elrgspnlem1  33207  elrgspnlem2  33208  elrgspnlem3  33209  elrgspnlem4  33210  elrgspn  33211  elrgspnsubrunlem1  33212  linds2eq  33344  elrspunidl  33391  elrspunsn  33392  evl1deg1  33537  evl1deg2  33538  evl1deg3  33539  mplvrpmfgalem  33572  mplvrpmga  33573  mplvrpmmhm  33574  mplvrpmrhm  33575  splysubrg  33581  issply  33582  esplyval  33583  lbsdiflsp0  33637  fedgmullem1  33640  fedgmullem2  33641  fedgmul  33642  evls1fldgencl  33681  fldextrspunlsplem  33684  fldextrspunlsp  33685  extdgfialglem2  33704  mdetpmtr1  33834  zar0ring  33889  ordtcnvNEW  33931  ordtrest2NEW  33934  xrhval  34029  esum2dlem  34103  ofceq  34108  itgeq12dv  34337  ballotlemfval  34501  vtsval  34648  lpadval  34687  ptpconn  35275  cvmliftlem15  35340  cvmlift2lem4  35348  cvmlift2  35358  snmlval  35373  snmlflim  35374  satf  35395  mrsubfval  35550  mrsubrn  35555  elmsubrn  35570  msubrn  35571  msubco  35573  faclim  35788  faclim2  35790  prodeq12sdv  36258  itgeq12sdv  36259  cbvsumdavw  36319  cbvproddavw  36320  cbvsumdavw2  36335  cbvproddavw2  36336  knoppcnlem1  36533  knoppcnlem6  36538  knoppcnlem7  36539  bj-evaleq  37112  csbrdgg  37369  curfv  37646  matunitlindflem2  37663  poimirlem5  37671  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem18  37684  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem27  37693  voliunnfl  37710  itg2addnclem  37717  itg2addnclem3  37719  itg2addnc  37720  itg2gt0cn  37721  iblabsnclem  37729  iblmulc2nc  37731  ftc1anclem2  37740  ftc1anclem6  37744  ftc1anclem8  37746  ftc1anc  37747  ftc2nc  37748  upixp  37775  rrncmslem  37878  ismrer1  37884  tendoplcbv  40820  tendopl  40821  tendoicbv  40838  tendoi  40839  dihfval  41276  lcfl7N  41546  lcfrlem8  41594  lcfrlem9  41595  lcf1o  41596  hvmapval  41805  hdmap1fval  41841  hdmapffval  41871  hdmapfval  41872  hgmapffval  41930  hgmapfval  41931  lcmineqlem7  42074  lcmineqlem12  42079  aks6d1c6lem5  42216  rhmpsr  42591  evlsvval  42599  evlsvvval  42602  evlsbagval  42605  selvvvval  42624  evlselv  42626  fsuppind  42629  fsuppssindlem2  42631  fsuppssind  42632  mzpclval  42764  mzpcl2  42769  mzpexpmpt  42784  mzpsubst  42787  mzpcompact2lem  42790  rmxfval  42943  rmyfval  42944  aomclem8  43100  hbtlem1  43162  hbtlem7  43164  rfovfvd  44041  fsovrfovd  44048  fsovfvd  44049  fsovcnvlem  44052  dssmapfv2d  44057  dssmapnvod  44059  ntrneibex  44112  mnringmulrvald  44266  mnringmulrcld  44267  expgrowthi  44372  expgrowth  44374  binomcxplemdvsum  44394  addrval  44504  subrval  44505  mulvval  44506  fmulcl  45627  fmuldfeqlem1  45628  fprodcnlem  45645  fprodcn  45646  fnlimfv  45707  fnlimcnv  45711  fnlimfvre  45718  fnlimfvre2  45721  fnlimf  45722  fnlimabslt  45723  liminfval  45803  limsupresxr  45810  liminfresxr  45811  liminfvalxr  45827  fprodcncf  45944  dvnmptdivc  45982  dvnxpaek  45986  dvnmul  45987  dvmptfprod  45989  dvnprodlem1  45990  dvnprodlem2  45991  dvnprodlem3  45992  dvnprod  45993  stoweidlem2  46046  stoweidlem17  46061  stoweidlem19  46063  stoweidlem20  46064  stoweidlem43  46087  stoweidlem62  46106  stoweid  46107  dirkercncflem2  46148  fourierdlem112  46262  fourierdlem113  46263  etransclem1  46279  etransclem5  46283  etransclem17  46295  etransclem19  46297  etransclem22  46300  sge0val  46410  ovnlecvr  46602  ovncvrrp  46608  ovn0lem  46609  ovnsubaddlem1  46614  ovnsubadd  46616  hsphoif  46620  hsphoival  46623  hoidmv1lelem1  46635  hoidmv1lelem2  46636  hoidmv1lelem3  46637  hoidmv1le  46638  hoidmvlelem1  46639  hoidmvlelem2  46640  hoidmvlelem3  46641  hoidmvlelem4  46642  hoidmvlelem5  46643  hoidmvle  46644  ovnhoilem1  46645  ovnhoi  46647  hoidifhspval  46652  ovncvr2  46655  hoidifhspval2  46659  hspmbllem2  46671  hspmbllem3  46672  hspmbl  46673  ovnovollem1  46700  vonioolem2  46725  vonioo  46726  vonicclem2  46728  vonicc  46729  smflimlem4  46818  smflim  46821  smflim2  46850  smfsuplem2  46856  smfsup  46858  smfinf  46862  smflimsuplem2  46865  smflimsuplem5  46868  smflimsuplem7  46870  smflimsup  46872  cfsetsnfsetfo  47097  lincop  48446  1arymaptfv  48678  itcoval  48699  itcovalpc  48710  itcovalt2  48715  ackvalsuc1mpt  48716  ackval1  48719  fuco21  49374  prcofval  49416  aacllem  49839