Theorem mpteq2dv 5198

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-mpt 5186

This theorem is used by:  ifmpt2v  7524  ofeqd  7697  mpocurryvald  8292  rdgeq1  8424  rdgeq2  8425  omv  8525  oev  8527  curfv  8897  oieq1  9511  oieq2  9512  cantnflem1  9695  wunex2  10828  wuncval2  10837  indval  12328  rpnnen1  13116  seqof2  14208  relexpsucnnr  15185  relexp1g  15186  limsupval  15648  sumeq2w  15866  sumeq2ii  15867  cbvsum  15869  cbvsumv  15870  sumeq2sdv  15877  summo  15890  fsum  15893  fsumrlim  15985  fsumo1  15986  prodeq1  16083  prodeq2w  16086  prodeq2sdv  16098  prodmo  16110  fprod  16115  bpolylem  16221  rpnnen2lem1  16389  rpnnen2lem2  16390  1arithlem1  17108  vdwapval  17158  vdwlem6  17171  vdwlem8  17173  vdwlem9  17174  vdwlem10  17175  ramub1lem2  17212  ramcl  17214  sloteq  17368  prdsplusgval  17651  prdsmulrval  17653  prdsdsval  17656  prdsvscaval  17657  ismon  17915  fucco  18147  curf1  18406  curf2  18410  yonedalem4a  18456  smndex1gbas  19105  smndex1gbasOLD  19106  smndex1gid  19107  smndex1gidOLD  19108  smndex1igid  19109  grplactfval  19258  galactghm  19625  pmtrval  19672  sylow1  19824  sylow2b  19844  sylow3lem5  19852  sylow3  19854  iscyg  20100  gsumzaddlem  20142  gsumzmhm  20158  ablfac2  20312  gsumdixp  20555  c0rhm  20793  c0rnghm  20794  zncyg  21861  phllmhm  21945  isphld  21967  frlmgsum  22085  frlmipval  22092  frlmphl  22094  uvcval  22098  fczpsrbag  22236  psrmulfval  22258  psrascl  22293  mvrval  22296  subrgmvr  22349  mplcoe1  22353  mplcoe3  22354  mplcoe5  22356  mplmon2  22377  subrgascl  22382  evlslem2  22395  evlslem3  22396  evlslem1  22398  mpfrcl  22401  evlsval  22402  evlsvval  22406  evlsvvval  22409  evlsvar  22411  mpfind  22431  selvfval  22435  selvval  22436  selvvvval  22458  mhpfval  22466  psdfval  22486  psdval  22487  psdmvr  22497  coe1fval  22530  pf1ind  22680  evl1gsumadd  22683  rhmmpl  22705  rhmply1vr1  22709  mamuval  22715  mamufv  22716  matgsum  22759  madetsumid  22783  mat1dimmul  22798  mvmulval  22865  mvmulfv  22866  mavmulfv  22868  1mavmul  22870  marepvval0  22888  mulmarep1gsum1  22895  mdetleib  22909  mdetleib2  22910  mdetfval1  22912  mdetleib1  22913  mdet0pr  22914  m1detdiag  22919  mdetralt  22930  mdetunilem9  22942  m2detleib  22953  smadiadetlem3  22990  matunitlindflem2  23002  mat2pmatmul  23056  decpmatmul  23097  decpmatmulsumfsupp  23098  pmatcollpw1  23101  monmatcollpw  23104  pmatcollpw3lem  23108  pmatcollpw3fi1lem2  23112  pm2mpval  23120  pm2mpfval  23121  mply1topmatval  23129  mp2pm2mplem1  23131  mp2pm2mplem3  23133  ptbasfi  23907  ptcnplem  23947  ptrescn  23965  cnmpt2k  24014  xkohmeo  24141  fmval  24269  fmf  24271  ptcmpg  24383  tmdmulg  24418  prdstmdd  24450  tsmspropd  24458  prdsxmslem2  24855  metdsval  25174  fsumcn  25198  expcn  25200  lebnumlem3  25291  pcoval  25339  pi1xfrcnv  25385  cphsscph  25579  rrxds  25721  rrxmval  25733  itg11  26019  mbfi1fseqlem2  26044  mbfi1fseqlem6  26048  mbfi1fseq  26049  mbfi1flimlem  26050  mbfmullem  26053  itg2const  26068  itg2mulc  26075  itg2monolem1  26078  itg2i1fseqle  26082  itg2i1fseq  26083  itg2addlem  26086  itg2cnlem1  26089  itg2cn  26091  isibl  26093  isibl2  26094  iblitg  26096  itgeq1  26100  itgz  26108  itgvallem  26112  itgvallem3  26113  iblcnlem1  26115  itgcnlem  26117  iblrelem  26118  iblposlem  26119  iblpos  26120  itgrevallem1  26122  itgposval  26123  iblss2  26133  itgss  26139  itgfsum  26154  iblabslem  26155  iblmulc2  26158  bddmulibl  26166  itgcn  26172  ellimc  26200  dvnfval  26249  cpnfval  26259  dvexp  26280  dvexp2  26281  dvmptfsum  26302  dvlipcn  26321  dvivthlem1  26335  dvfsumle  26348  dvfsumabs  26350  dvfsumlem2  26354  itgpowd  26377  elply2  26521  elplyr  26526  elplyd  26527  coeeu  26551  coelem  26552  coeeq  26553  plyco  26567  coe11  26579  coe1termlem  26584  dgrcolem1  26599  dvply2g  26613  elqaalem3  26651  eltayl  26694  tayl0  26696  taylthlem1  26707  taylthlem2  26708  ulmcau  26729  ulmdvlem1  26734  ulmdvlem3  26736  mtest  26738  mtestbdd  26739  pserval  26744  pserulm  26756  psercn  26760  pserdvlem2  26762  abelthlem3  26767  logtayl  26995  dvcxp1  27075  dvcncxp1  27078  logbmpt  27123  dmarea  27292  lgamgulmlem2  27364  lgamgulmlem5  27367  musum  27525  dchrptlem2  27599  dchrptlem3  27600  dchrpt  27601  lgsval  27635  lgsval4lem  27642  lgsneg  27655  lgsmod  27657  rpvmasum2  27846  padicfval  27950  ostth2  27971  ostth3  27972  ostth  27973  lmif  29297  islmib  29299  incistruhgr  29664  eucrct2eupth  30853  htthlem  31526  htth  31527  pjhfval  32005  hosmval  32344  hommval  32345  hodmval  32346  hfsmval  32347  hfmmval  32348  brafval  32552  kbfval  32561  mptprop  33340  indsn  33478  psgnfzto1st  33714  fxpsubm  33781  fxpsubg  33782  fxpsubrg  33783  elrgspnlem1  33851  elrgspnlem2  33852  elrgspnlem3  33853  elrgspnlem4  33854  elrgspn  33855  elrgspnsubrunlem1  33856  linds2eq  33984  elrspunidl  34026  elrspunsn  34027  evl1deg1  34156  evl1deg2  34157  evl1deg3  34158  mplasclco  34196  selvply1rhmlema  34198  selvply1rhmlemb  34199  selvply1rhmlem2  34201  selvply1rhmlem3  34202  selvply1rhmlem4  34203  selvply1rhmlem5  34204  selvply1rhm  34205  mplidom  34208  extvfval  34212  extvfv  34213  mvrvalind  34218  evlextv  34222  mplvrpmfgalem  34224  mplvrpmga  34225  mplvrpmmhm  34226  mplvrpmrhm  34227  psrgsum  34228  psrmonmul2  34231  psrmonprod  34232  splysubrg  34240  issply  34241  esplyval  34242  esplyfvaln  34254  vietalem  34259  vieta  34260  lbsdiflsp0  34306  fedgmullem1  34309  fedgmullem2  34310  fedgmul  34311  evls1fldgencl  34350  fldextrspunlsplem  34353  fldextrspunlsp  34354  extdgfialglem2  34373  mdetpmtr1  34503  zar0ring  34558  ordtcnvNEW  34600  ordtrest2NEW  34603  xrhval  34698  esum2dlem  34772  ofceq  34777  itgeq12dv  35006  ballotlemfval  35170  vtsval  35314  lpadval  35356  ptpconn  36086  cvmliftlem15  36151  cvmlift2lem4  36159  cvmlift2  36169  snmlval  36184  snmlflim  36185  satf  36206  mrsubfval  36361  mrsubrn  36366  elmsubrn  36381  msubrn  36382  msubco  36384  faclim  36605  faclim2  36607  prodeq12sdv  37101  itgeq12sdv  37102  cbvsumdavw  37162  cbvproddavw  37163  cbvsumdavw2  37178  cbvproddavw2  37179  knoppcnlem1  37453  knoppcnlem6  37458  knoppcnlem7  37459  bj-evaleq  38098  csbrdgg  38359  poimirlem5  38650  poimirlem6  38651  poimirlem7  38652  poimirlem8  38653  poimirlem10  38655  poimirlem11  38656  poimirlem12  38657  poimirlem15  38660  poimirlem16  38661  poimirlem17  38662  poimirlem18  38663  poimirlem19  38664  poimirlem20  38665  poimirlem21  38666  poimirlem22  38667  poimirlem27  38672  voliunnfl  38689  itg2addnclem  38696  itg2addnclem3  38698  itg2addnc  38699  itg2gt0cn  38700  iblabsnclem  38708  iblmulc2nc  38710  ftc1anclem2  38719  ftc1anclem6  38723  ftc1anclem8  38725  ftc1anc  38726  ftc2nc  38727  upixp  38770  rrncmslem  38873  ismrer1  38879  tendoplcbv  41939  tendopl  41940  tendoicbv  41957  tendoi  41958  dihfval  42395  lcfl7N  42665  lcfrlem8  42713  lcfrlem9  42714  lcf1o  42715  hvmapval  42924  hdmap1fval  42960  hdmapffval  42990  hdmapfval  42991  hgmapffval  43049  hgmapfval  43050  lcmineqlem7  43192  lcmineqlem12  43197  aks6d1c6lem5  43334  rhmpsr  43718  evlsbagval  43721  evlselv  43724  fsuppind  43725  fsuppssindlem2  43727  fsuppssind  43728  mzpclval  43843  mzpcl2  43848  mzpexpmpt  43863  mzpsubst  43866  mzpcompact2lem  43869  rmxfval  44018  rmyfval  44019  aomclem8  44170  hbtlem1  44232  hbtlem7  44234  rfovfvd  45109  fsovrfovd  45116  fsovfvd  45117  fsovcnvlem  45120  dssmapfv2d  45125  dssmapnvod  45127  ntrneibex  45180  mnringmulrvald  45332  mnringmulrcld  45333  expgrowthi  45424  expgrowth  45426  binomcxplemdvsum  45446  addrval  45555  subrval  45556  mulvval  45557  fmulcl  46700  fmuldfeqlem1  46701  fprodcnlem  46718  fprodcn  46719  fnlimfv  46780  fnlimcnv  46784  fnlimfvre  46791  fnlimfvre2  46794  fnlimf  46795  fnlimabslt  46796  liminfval  46876  limsupresxr  46883  liminfresxr  46884  liminfvalxr  46900  fprodcncf  47017  dvnmptdivc  47055  dvnxpaek  47059  dvnmul  47060  dvmptfprod  47062  dvnprodlem1  47063  dvnprodlem2  47064  dvnprodlem3  47065  dvnprod  47066  stoweidlem2  47119  stoweidlem17  47134  stoweidlem19  47136  stoweidlem20  47137  stoweidlem43  47160  stoweidlem62  47179  stoweid  47180  dirkercncflem2  47221  fourierdlem112  47335  fourierdlem113  47336  etransclem1  47352  etransclem5  47356  etransclem17  47368  etransclem19  47370  etransclem22  47373  sge0val  47483  ovnlecvr  47675  ovncvrrp  47681  ovn0lem  47682  ovnsubaddlem1  47687  ovnsubadd  47689  hsphoif  47693  hsphoival  47696  hoidmv1lelem1  47708  hoidmv1lelem2  47709  hoidmv1lelem3  47710  hoidmv1le  47711  hoidmvlelem1  47712  hoidmvlelem2  47713  hoidmvlelem3  47714  hoidmvlelem4  47715  hoidmvlelem5  47716  hoidmvle  47717  ovnhoilem1  47718  ovnhoi  47720  hoidifhspval  47725  ovncvr2  47728  hoidifhspval2  47732  hspmbllem2  47744  hspmbllem3  47745  hspmbl  47746  ovnovollem1  47773  vonioolem2  47798  vonioo  47799  vonicclem2  47801  vonicc  47802  smflimlem4  47891  smflim  47894  smflim2  47923  smfsuplem2  47929  smfsup  47931  smfinf  47935  smflimsuplem2  47938  smflimsuplem5  47941  smflimsuplem7  47943  smflimsup  47945  cfsetsnfsetfo  48237  lincop  49627  1arymaptfv  49859  itcoval  49880  itcovalpc  49891  itcovalt2  49896  ackvalsuc1mpt  49897  ackval1  49900  fuco21  50565  postcof2  50607  prcofval  50620  aacllem  51121  crosspval  51136  crosspdot0lem  51145  veronesevald  51153  veronesematrowexpd  51164