Theorem mpteq2dv 5206

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 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5205	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5175  df-mpt 5194

This theorem is referenced by:  ifmpt2v  7510  ofeqd  7674  mpocurryvald  8262  rdgeq1  8394  rdgeq2  8395  omv  8493  oev  8495  oieq1  9470  oieq2  9471  cantnflem1  9654  wunex2  10719  wuncval2  10728  indval  12217  rpnnen1  13003  seqof2  14092  relexpsucnnr  15058  relexp1g  15059  limsupval  15521  sumeq2w  15739  sumeq2ii  15740  cbvsum  15742  cbvsumv  15743  sumeq2sdv  15750  summo  15764  fsum  15767  fsumrlim  15859  fsumo1  15860  prodeq1  15957  prodeq2w  15960  prodeq2sdv  15973  prodmo  15986  fprod  15991  bpolylem  16098  rpnnen2lem1  16266  rpnnen2lem2  16267  1arithlem1  16979  vdwapval  17029  vdwlem6  17042  vdwlem8  17044  vdwlem9  17045  vdwlem10  17046  ramub1lem2  17083  ramcl  17085  sloteq  17239  prdsplusgval  17522  prdsmulrval  17524  prdsdsval  17527  prdsvscaval  17528  ismon  17786  fucco  18018  curf1  18277  curf2  18281  yonedalem4a  18327  smndex1gbas  18957  smndex1gbasOLD  18958  smndex1gid  18959  smndex1gidOLD  18960  smndex1igid  18961  grplactfval  19103  galactghm  19470  pmtrval  19517  sylow1  19669  sylow2b  19689  sylow3lem5  19697  sylow3  19699  iscyg  19945  gsumzaddlem  19987  gsumzmhm  20003  ablfac2  20157  gsumdixp  20396  c0rhm  20615  c0rnghm  20616  zncyg  21663  phllmhm  21747  isphld  21769  frlmgsum  21887  frlmipval  21894  frlmphl  21896  uvcval  21900  fczpsrbag  22036  psrmulfval  22058  psrascl  22093  mvrval  22096  subrgmvr  22149  mplcoe1  22153  mplcoe3  22154  mplcoe5  22156  mplmon2  22177  subrgascl  22182  evlslem2  22195  evlslem3  22196  evlslem1  22198  mpfrcl  22201  evlsval  22202  evlsvval  22206  evlsvvval  22209  evlsvar  22211  mpfind  22231  selvfval  22235  selvval  22236  selvvvval  22258  mhpfval  22266  psdfval  22286  psdval  22287  psdmvr  22297  coe1fval  22330  pf1ind  22480  evl1gsumadd  22483  rhmmpl  22505  rhmply1vr1  22509  mamuval  22515  mamufv  22516  matgsum  22559  madetsumid  22583  mat1dimmul  22598  mvmulval  22665  mvmulfv  22666  mavmulfv  22668  1mavmul  22670  marepvval0  22688  mulmarep1gsum1  22695  mdetleib  22709  mdetleib2  22710  mdetfval1  22712  mdetleib1  22713  mdet0pr  22714  m1detdiag  22719  mdetralt  22730  mdetunilem9  22742  m2detleib  22753  smadiadetlem3  22790  mat2pmatmul  22853  decpmatmul  22894  decpmatmulsumfsupp  22895  pmatcollpw1  22898  monmatcollpw  22901  pmatcollpw3lem  22905  pmatcollpw3fi1lem2  22909  pm2mpval  22917  pm2mpfval  22918  mply1topmatval  22926  mp2pm2mplem1  22928  mp2pm2mplem3  22930  ptbasfi  23703  ptcnplem  23743  ptrescn  23761  cnmpt2k  23810  xkohmeo  23937  fmval  24065  fmf  24067  ptcmpg  24179  tmdmulg  24214  prdstmdd  24246  tsmspropd  24254  prdsxmslem2  24651  metdsval  24970  fsumcn  24994  expcn  24996  lebnumlem3  25087  pcoval  25135  pi1xfrcnv  25181  cphsscph  25375  rrxds  25517  rrxmval  25529  itg11  25815  mbfi1fseqlem2  25840  mbfi1fseqlem6  25844  mbfi1fseq  25845  mbfi1flimlem  25846  mbfmullem  25849  itg2const  25864  itg2mulc  25871  itg2monolem1  25874  itg2i1fseqle  25878  itg2i1fseq  25879  itg2addlem  25882  itg2cnlem1  25885  itg2cn  25887  isibl  25889  isibl2  25890  iblitg  25892  itgeq1  25897  itgz  25905  itgvallem  25909  itgvallem3  25910  iblcnlem1  25912  itgcnlem  25914  iblrelem  25915  iblposlem  25916  iblpos  25917  itgrevallem1  25919  itgposval  25920  iblss2  25930  itgss  25936  itgfsum  25951  iblabslem  25952  iblmulc2  25955  bddmulibl  25963  itgcn  25969  ellimc  25997  dvnfval  26046  cpnfval  26056  dvexp  26077  dvexp2  26078  dvmptfsum  26099  dvlipcn  26118  dvivthlem1  26132  dvfsumle  26145  dvfsumabs  26147  dvfsumlem2  26151  itgpowd  26174  elply2  26318  elplyr  26323  elplyd  26324  coeeu  26347  coelem  26348  coeeq  26349  plyco  26363  coe11  26375  coe1termlem  26380  dgrcolem1  26395  dvply2g  26411  elqaalem3  26447  eltayl  26485  tayl0  26487  taylthlem1  26498  taylthlem2  26499  ulmcau  26520  ulmdvlem1  26525  ulmdvlem3  26527  mtest  26529  mtestbdd  26530  pserval  26535  pserulm  26547  psercn  26551  pserdvlem2  26553  abelthlem3  26558  logtayl  26787  dvcxp1  26867  dvcncxp1  26870  logbmpt  26915  dmarea  27084  lgamgulmlem2  27156  lgamgulmlem5  27159  musum  27317  dchrptlem2  27391  dchrptlem3  27392  dchrpt  27393  lgsval  27427  lgsval4lem  27434  lgsneg  27447  lgsmod  27449  rpvmasum2  27638  padicfval  27742  ostth2  27763  ostth3  27764  ostth  27765  lmif  29048  islmib  29050  incistruhgr  29366  eucrct2eupth  30533  htthlem  31206  htth  31207  pjhfval  31685  hosmval  32024  hommval  32025  hodmval  32026  hfsmval  32027  hfmmval  32028  brafval  32232  kbfval  32241  mptprop  32980  indsn  33120  psgnfzto1st  33362  fxpsubm  33429  fxpsubg  33430  fxpsubrg  33431  elrgspnlem1  33499  elrgspnlem2  33500  elrgspnlem3  33501  elrgspnlem4  33502  elrgspn  33503  elrgspnsubrunlem1  33504  linds2eq  33634  elrspunidl  33676  elrspunsn  33677  evl1deg1  33807  evl1deg2  33808  evl1deg3  33809  mplasclco  33847  selvply1rhmlema  33849  selvply1rhmlemb  33850  selvply1rhmlem2  33852  selvply1rhmlem3  33853  selvply1rhmlem4  33854  selvply1rhmlem5  33855  selvply1rhm  33856  mplidom  33859  extvfval  33863  extvfv  33864  mvrvalind  33869  evlextv  33873  mplvrpmfgalem  33875  mplvrpmga  33876  mplvrpmmhm  33877  mplvrpmrhm  33878  psrgsum  33879  psrmonmul2  33882  psrmonprod  33883  splysubrg  33891  issply  33892  esplyval  33893  esplyfvaln  33905  vietalem  33910  vieta  33911  lbsdiflsp0  33957  fedgmullem1  33960  fedgmullem2  33961  fedgmul  33962  evls1fldgencl  34001  fldextrspunlsplem  34004  fldextrspunlsp  34005  extdgfialglem2  34024  mdetpmtr1  34154  zar0ring  34209  ordtcnvNEW  34251  ordtrest2NEW  34254  xrhval  34349  esum2dlem  34423  ofceq  34428  itgeq12dv  34657  ballotlemfval  34821  vtsval  34965  lpadval  35007  ptpconn  35620  cvmliftlem15  35685  cvmlift2lem4  35693  cvmlift2  35703  snmlval  35718  snmlflim  35719  satf  35740  mrsubfval  35895  mrsubrn  35900  elmsubrn  35915  msubrn  35916  msubco  35918  faclim  36133  faclim2  36135  prodeq12sdv  36615  itgeq12sdv  36616  cbvsumdavw  36676  cbvproddavw  36677  cbvsumdavw2  36692  cbvproddavw2  36693  knoppcnlem1  36967  knoppcnlem6  36972  knoppcnlem7  36973  bj-evaleq  37596  csbrdgg  37858  curfv  38134  matunitlindflem2  38151  poimirlem5  38159  poimirlem6  38160  poimirlem7  38161  poimirlem8  38162  poimirlem10  38164  poimirlem11  38165  poimirlem12  38166  poimirlem15  38169  poimirlem16  38170  poimirlem17  38171  poimirlem18  38172  poimirlem19  38173  poimirlem20  38174  poimirlem21  38175  poimirlem22  38176  poimirlem27  38181  voliunnfl  38198  itg2addnclem  38205  itg2addnclem3  38207  itg2addnc  38208  itg2gt0cn  38209  iblabsnclem  38217  iblmulc2nc  38219  ftc1anclem2  38228  ftc1anclem6  38232  ftc1anclem8  38234  ftc1anc  38235  ftc2nc  38236  upixp  38263  rrncmslem  38366  ismrer1  38372  tendoplcbv  41434  tendopl  41435  tendoicbv  41452  tendoi  41453  dihfval  41890  lcfl7N  42160  lcfrlem8  42208  lcfrlem9  42209  lcf1o  42210  hvmapval  42419  hdmap1fval  42455  hdmapffval  42485  hdmapfval  42486  hgmapffval  42544  hgmapfval  42545  lcmineqlem7  42687  lcmineqlem12  42692  aks6d1c6lem5  42829  rhmpsr  43202  evlsbagval  43205  evlselv  43208  fsuppind  43209  fsuppssindlem2  43211  fsuppssind  43212  mzpclval  43343  mzpcl2  43348  mzpexpmpt  43363  mzpsubst  43366  mzpcompact2lem  43369  rmxfval  43518  rmyfval  43519  aomclem8  43675  hbtlem1  43737  hbtlem7  43739  rfovfvd  44615  fsovrfovd  44622  fsovfvd  44623  fsovcnvlem  44626  dssmapfv2d  44631  dssmapnvod  44633  ntrneibex  44686  mnringmulrvald  44838  mnringmulrcld  44839  expgrowthi  44930  expgrowth  44932  binomcxplemdvsum  44952  addrval  45061  subrval  45062  mulvval  45063  fmulcl  46184  fmuldfeqlem1  46185  fprodcnlem  46202  fprodcn  46203  fnlimfv  46264  fnlimcnv  46268  fnlimfvre  46275  fnlimfvre2  46278  fnlimf  46279  fnlimabslt  46280  liminfval  46360  limsupresxr  46367  liminfresxr  46368  liminfvalxr  46384  fprodcncf  46501  dvnmptdivc  46539  dvnxpaek  46543  dvnmul  46544  dvmptfprod  46546  dvnprodlem1  46547  dvnprodlem2  46548  dvnprodlem3  46549  dvnprod  46550  stoweidlem2  46603  stoweidlem17  46618  stoweidlem19  46620  stoweidlem20  46621  stoweidlem43  46644  stoweidlem62  46663  stoweid  46664  dirkercncflem2  46705  fourierdlem112  46819  fourierdlem113  46820  etransclem1  46836  etransclem5  46840  etransclem17  46852  etransclem19  46854  etransclem22  46857  sge0val  46967  ovnlecvr  47159  ovncvrrp  47165  ovn0lem  47166  ovnsubaddlem1  47171  ovnsubadd  47173  hsphoif  47177  hsphoival  47180  hoidmv1lelem1  47192  hoidmv1lelem2  47193  hoidmv1lelem3  47194  hoidmv1le  47195  hoidmvlelem1  47196  hoidmvlelem2  47197  hoidmvlelem3  47198  hoidmvlelem4  47199  hoidmvlelem5  47200  hoidmvle  47201  ovnhoilem1  47202  ovnhoi  47204  hoidifhspval  47209  ovncvr2  47212  hoidifhspval2  47216  hspmbllem2  47228  hspmbllem3  47229  hspmbl  47230  ovnovollem1  47257  vonioolem2  47282  vonioo  47283  vonicclem2  47285  vonicc  47286  smflimlem4  47375  smflim  47378  smflim2  47407  smfsuplem2  47413  smfsup  47415  smfinf  47419  smflimsuplem2  47422  smflimsuplem5  47425  smflimsuplem7  47427  smflimsup  47429  cfsetsnfsetfo  47681  lincop  49068  1arymaptfv  49300  itcoval  49321  itcovalpc  49332  itcovalt2  49337  ackvalsuc1mpt  49338  ackval1  49341  fuco21  49994  prcofval  50036  aacllem  50470