Theorem mpteq2dv 5244

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5225

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-mpt 5226

This theorem is referenced by:  ifmpt2v  7535  ofeqd  7699  mpocurryvald  8295  rdgeq1  8451  rdgeq2  8452  omv  8550  oev  8552  oieq1  9552  oieq2  9553  cantnflem1  9729  wunex2  10778  wuncval2  10787  rpnnen1  13025  seqof2  14101  relexpsucnnr  15064  relexp1g  15065  limsupval  15510  sumeq2w  15728  sumeq2ii  15729  cbvsum  15731  cbvsumv  15732  sumeq2sdv  15739  summo  15753  fsum  15756  fsumrlim  15847  fsumo1  15848  prodeq1  15943  prodeq2w  15946  prodeq2sdv  15959  prodmo  15972  fprod  15977  bpolylem  16084  rpnnen2lem1  16250  rpnnen2lem2  16251  1arithlem1  16961  vdwapval  17011  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  vdwlem10  17028  ramub1lem2  17065  ramcl  17067  sloteq  17220  prdsplusgval  17518  prdsmulrval  17520  prdsdsval  17523  prdsvscaval  17524  ismon  17777  fucco  18010  curf1  18270  curf2  18274  yonedalem4a  18320  smndex1gbas  18915  smndex1gid  18916  grplactfval  19059  galactghm  19422  pmtrval  19469  sylow1  19621  sylow2b  19641  sylow3lem5  19649  sylow3  19651  iscyg  19897  gsumzaddlem  19939  gsumzmhm  19955  ablfac2  20109  gsumdixp  20316  c0rhm  20534  c0rnghm  20535  zncyg  21567  phllmhm  21650  isphld  21672  frlmgsum  21792  frlmipval  21799  frlmphl  21801  uvcval  21805  fczpsrbag  21941  psrmulfval  21963  psrascl  21999  mvrval  22002  subrgmvr  22051  mplcoe1  22055  mplcoe3  22056  mplcoe5  22058  mplmon2  22085  subrgascl  22090  evlslem2  22103  evlslem3  22104  evlslem1  22106  mpfrcl  22109  evlsval  22110  evlsvar  22114  mpfind  22131  selvfval  22138  selvval  22139  mhpfval  22142  psdfval  22162  psdval  22163  psdmvr  22173  coe1fval  22207  pf1ind  22359  evl1gsumadd  22362  rhmmpl  22387  rhmply1vr1  22391  mamuval  22397  mamufv  22398  matgsum  22443  madetsumid  22467  mat1dimmul  22482  mvmulval  22549  mvmulfv  22550  mavmulfv  22552  1mavmul  22554  marepvval0  22572  mulmarep1gsum1  22579  mdetleib  22593  mdetleib2  22594  mdetfval1  22596  mdetleib1  22597  mdet0pr  22598  m1detdiag  22603  mdetralt  22614  mdetunilem9  22626  m2detleib  22637  smadiadetlem3  22674  mat2pmatmul  22737  decpmatmul  22778  decpmatmulsumfsupp  22779  pmatcollpw1  22782  monmatcollpw  22785  pmatcollpw3lem  22789  pmatcollpw3fi1lem2  22793  pm2mpval  22801  pm2mpfval  22802  mply1topmatval  22810  mp2pm2mplem1  22812  mp2pm2mplem3  22814  ptbasfi  23589  ptcnplem  23629  ptrescn  23647  cnmpt2k  23696  xkohmeo  23823  fmval  23951  fmf  23953  ptcmpg  24065  tmdmulg  24100  prdstmdd  24132  tsmspropd  24140  prdsxmslem2  24542  metdsval  24869  fsumcn  24894  expcn  24896  expcnOLD  24898  lebnumlem3  24995  pcoval  25044  pi1xfrcnv  25090  cphsscph  25285  rrxds  25427  rrxmval  25439  itg11  25726  mbfi1fseqlem2  25751  mbfi1fseqlem6  25755  mbfi1fseq  25756  mbfi1flimlem  25757  mbfmullem  25760  itg2const  25775  itg2mulc  25782  itg2monolem1  25785  itg2i1fseqle  25789  itg2i1fseq  25790  itg2addlem  25793  itg2cnlem1  25796  itg2cn  25798  isibl  25800  isibl2  25801  iblitg  25803  itgeq1  25808  itgz  25816  itgvallem  25820  itgvallem3  25821  iblcnlem1  25823  itgcnlem  25825  iblrelem  25826  iblposlem  25827  iblpos  25828  itgrevallem1  25830  itgposval  25831  iblss2  25841  itgss  25847  itgfsum  25862  iblabslem  25863  iblmulc2  25866  bddmulibl  25874  itgcn  25880  ellimc  25908  dvnfval  25958  cpnfval  25968  dvexp  25991  dvexp2  25992  dvmptfsum  26013  dvlipcn  26033  dvivthlem1  26047  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgpowd  26091  elply2  26235  elplyr  26240  elplyd  26241  coeeu  26264  coelem  26265  coeeq  26266  plyco  26280  coe11  26292  coe1termlem  26297  dgrcolem1  26313  dvply2g  26326  dvply2gOLD  26327  elqaalem3  26363  eltayl  26401  tayl0  26403  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmcau  26438  ulmdvlem1  26443  ulmdvlem3  26445  mtest  26447  mtestbdd  26448  pserval  26453  pserulm  26465  psercn  26470  pserdvlem2  26472  abelthlem3  26477  logtayl  26702  dvcxp1  26782  dvcncxp1  26785  logbmpt  26831  dmarea  27000  lgamgulmlem2  27073  lgamgulmlem5  27076  musum  27234  dchrptlem2  27309  dchrptlem3  27310  dchrpt  27311  lgsval  27345  lgsval4lem  27352  lgsneg  27365  lgsmod  27367  rpvmasum2  27556  padicfval  27660  ostth2  27681  ostth3  27682  ostth  27683  lmif  28793  islmib  28795  incistruhgr  29096  eucrct2eupth  30264  htthlem  30936  htth  30937  pjhfval  31415  hosmval  31754  hommval  31755  hodmval  31756  hfsmval  31757  hfmmval  31758  brafval  31962  kbfval  31971  mptprop  32707  indval  32838  psgnfzto1st  33125  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspn  33250  elrgspnsubrunlem1  33251  linds2eq  33409  elrspunidl  33456  elrspunsn  33457  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  evls1fldgencl  33720  fldextrspunlsplem  33723  fldextrspunlsp  33724  mdetpmtr1  33822  zar0ring  33877  ordtcnvNEW  33919  ordtrest2NEW  33922  xrhval  34019  esum2dlem  34093  ofceq  34098  itgeq12dv  34328  ballotlemfval  34492  vtsval  34652  lpadval  34691  ptpconn  35238  cvmliftlem15  35303  cvmlift2lem4  35311  cvmlift2  35321  snmlval  35336  snmlflim  35337  satf  35358  mrsubfval  35513  mrsubrn  35518  elmsubrn  35533  msubrn  35534  msubco  35536  faclim  35746  faclim2  35748  prodeq12sdv  36219  itgeq12sdv  36220  cbvsumdavw  36280  cbvproddavw  36281  cbvsumdavw2  36296  cbvproddavw2  36297  knoppcnlem1  36494  knoppcnlem6  36499  knoppcnlem7  36500  bj-evaleq  37073  csbrdgg  37330  curfv  37607  matunitlindflem2  37624  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem27  37654  voliunnfl  37671  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  iblabsnclem  37690  iblmulc2nc  37692  ftc1anclem2  37701  ftc1anclem6  37705  ftc1anclem8  37707  ftc1anc  37708  ftc2nc  37709  upixp  37736  rrncmslem  37839  ismrer1  37845  tendoplcbv  40777  tendopl  40778  tendoicbv  40795  tendoi  40796  dihfval  41233  lcfl7N  41503  lcfrlem8  41551  lcfrlem9  41552  lcf1o  41553  hvmapval  41762  hdmap1fval  41798  hdmapffval  41828  hdmapfval  41829  hgmapffval  41887  hgmapfval  41888  lcmineqlem7  42036  lcmineqlem12  42041  aks6d1c6lem5  42178  rhmpsr  42562  evlsvval  42570  evlsvvval  42573  evlsbagval  42576  selvvvval  42595  evlselv  42597  fsuppind  42600  fsuppssindlem2  42602  fsuppssind  42603  mzpclval  42736  mzpcl2  42741  mzpexpmpt  42756  mzpsubst  42759  mzpcompact2lem  42762  rmxfval  42915  rmyfval  42916  aomclem8  43073  hbtlem1  43135  hbtlem7  43137  rfovfvd  44015  fsovrfovd  44022  fsovfvd  44023  fsovcnvlem  44026  dssmapfv2d  44031  dssmapnvod  44033  ntrneibex  44086  mnringmulrvald  44246  mnringmulrcld  44247  expgrowthi  44352  expgrowth  44354  binomcxplemdvsum  44374  addrval  44485  subrval  44486  mulvval  44487  fmulcl  45596  fmuldfeqlem1  45597  fprodcnlem  45614  fprodcn  45615  fnlimfv  45678  fnlimcnv  45682  fnlimfvre  45689  fnlimfvre2  45692  fnlimf  45693  fnlimabslt  45694  liminfval  45774  limsupresxr  45781  liminfresxr  45782  liminfvalxr  45798  fprodcncf  45915  dvnmptdivc  45953  dvnxpaek  45957  dvnmul  45958  dvmptfprod  45960  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  dvnprod  45964  stoweidlem2  46017  stoweidlem17  46032  stoweidlem19  46034  stoweidlem20  46035  stoweidlem43  46058  stoweidlem62  46077  stoweid  46078  dirkercncflem2  46119  fourierdlem112  46233  fourierdlem113  46234  etransclem1  46250  etransclem5  46254  etransclem17  46266  etransclem19  46268  etransclem22  46271  sge0val  46381  ovnlecvr  46573  ovncvrrp  46579  ovn0lem  46580  ovnsubaddlem1  46585  ovnsubadd  46587  hsphoif  46591  hsphoival  46594  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvlelem5  46614  hoidmvle  46615  ovnhoilem1  46616  ovnhoi  46618  hoidifhspval  46623  ovncvr2  46626  hoidifhspval2  46630  hspmbllem2  46642  hspmbllem3  46643  hspmbl  46644  ovnovollem1  46671  vonioolem2  46696  vonioo  46697  vonicclem2  46699  vonicc  46700  smflimlem4  46789  smflim  46792  smflim2  46821  smfsuplem2  46827  smfsup  46829  smfinf  46833  smflimsuplem2  46836  smflimsuplem5  46839  smflimsuplem7  46841  smflimsup  46843  cfsetsnfsetfo  47072  lincop  48325  1arymaptfv  48561  itcoval  48582  itcovalpc  48593  itcovalt2  48598  ackvalsuc1mpt  48599  ackval1  48602  fuco21  49031  aacllem  49320