Theorem mpteq2dv 5189

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

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

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 5158  df-mpt 5177

This theorem is referenced by:  ifmpt2v  7455  ofeqd  7619  mpocurryvald  8210  rdgeq1  8340  rdgeq2  8341  omv  8437  oev  8439  oieq1  9423  oieq2  9424  cantnflem1  9604  wunex2  10651  wuncval2  10660  rpnnen1  12902  seqof2  13985  relexpsucnnr  14950  relexp1g  14951  limsupval  15399  sumeq2w  15617  sumeq2ii  15618  cbvsum  15620  cbvsumv  15621  sumeq2sdv  15628  summo  15642  fsum  15645  fsumrlim  15736  fsumo1  15737  prodeq1  15832  prodeq2w  15835  prodeq2sdv  15848  prodmo  15861  fprod  15866  bpolylem  15973  rpnnen2lem1  16141  rpnnen2lem2  16142  1arithlem1  16853  vdwapval  16903  vdwlem6  16916  vdwlem8  16918  vdwlem9  16919  vdwlem10  16920  ramub1lem2  16957  ramcl  16959  sloteq  17112  prdsplusgval  17395  prdsmulrval  17397  prdsdsval  17400  prdsvscaval  17401  ismon  17658  fucco  17890  curf1  18149  curf2  18153  yonedalem4a  18199  smndex1gbas  18794  smndex1gid  18795  grplactfval  18938  galactghm  19301  pmtrval  19348  sylow1  19500  sylow2b  19520  sylow3lem5  19528  sylow3  19530  iscyg  19776  gsumzaddlem  19818  gsumzmhm  19834  ablfac2  19988  gsumdixp  20222  c0rhm  20437  c0rnghm  20438  zncyg  21473  phllmhm  21557  isphld  21579  frlmgsum  21697  frlmipval  21704  frlmphl  21706  uvcval  21710  fczpsrbag  21846  psrmulfval  21868  psrascl  21904  mvrval  21907  subrgmvr  21956  mplcoe1  21960  mplcoe3  21961  mplcoe5  21963  mplmon2  21984  subrgascl  21989  evlslem2  22002  evlslem3  22003  evlslem1  22005  mpfrcl  22008  evlsval  22009  evlsvar  22013  mpfind  22030  selvfval  22037  selvval  22038  mhpfval  22041  psdfval  22061  psdval  22062  psdmvr  22072  coe1fval  22106  pf1ind  22258  evl1gsumadd  22261  rhmmpl  22286  rhmply1vr1  22290  mamuval  22296  mamufv  22297  matgsum  22340  madetsumid  22364  mat1dimmul  22379  mvmulval  22446  mvmulfv  22447  mavmulfv  22449  1mavmul  22451  marepvval0  22469  mulmarep1gsum1  22476  mdetleib  22490  mdetleib2  22491  mdetfval1  22493  mdetleib1  22494  mdet0pr  22495  m1detdiag  22500  mdetralt  22511  mdetunilem9  22523  m2detleib  22534  smadiadetlem3  22571  mat2pmatmul  22634  decpmatmul  22675  decpmatmulsumfsupp  22676  pmatcollpw1  22679  monmatcollpw  22682  pmatcollpw3lem  22686  pmatcollpw3fi1lem2  22690  pm2mpval  22698  pm2mpfval  22699  mply1topmatval  22707  mp2pm2mplem1  22709  mp2pm2mplem3  22711  ptbasfi  23484  ptcnplem  23524  ptrescn  23542  cnmpt2k  23591  xkohmeo  23718  fmval  23846  fmf  23848  ptcmpg  23960  tmdmulg  23995  prdstmdd  24027  tsmspropd  24035  prdsxmslem2  24433  metdsval  24752  fsumcn  24777  expcn  24779  expcnOLD  24781  lebnumlem3  24878  pcoval  24927  pi1xfrcnv  24973  cphsscph  25167  rrxds  25309  rrxmval  25321  itg11  25608  mbfi1fseqlem2  25633  mbfi1fseqlem6  25637  mbfi1fseq  25638  mbfi1flimlem  25639  mbfmullem  25642  itg2const  25657  itg2mulc  25664  itg2monolem1  25667  itg2i1fseqle  25671  itg2i1fseq  25672  itg2addlem  25675  itg2cnlem1  25678  itg2cn  25680  isibl  25682  isibl2  25683  iblitg  25685  itgeq1  25690  itgz  25698  itgvallem  25702  itgvallem3  25703  iblcnlem1  25705  itgcnlem  25707  iblrelem  25708  iblposlem  25709  iblpos  25710  itgrevallem1  25712  itgposval  25713  iblss2  25723  itgss  25729  itgfsum  25744  iblabslem  25745  iblmulc2  25748  bddmulibl  25756  itgcn  25762  ellimc  25790  dvnfval  25840  cpnfval  25850  dvexp  25873  dvexp2  25874  dvmptfsum  25895  dvlipcn  25915  dvivthlem1  25929  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumlem2  25949  dvfsumlem2OLD  25950  itgpowd  25973  elply2  26117  elplyr  26122  elplyd  26123  coeeu  26146  coelem  26147  coeeq  26148  plyco  26162  coe11  26174  coe1termlem  26179  dgrcolem1  26195  dvply2g  26208  dvply2gOLD  26209  elqaalem3  26245  eltayl  26283  tayl0  26285  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  ulmcau  26320  ulmdvlem1  26325  ulmdvlem3  26327  mtest  26329  mtestbdd  26330  pserval  26335  pserulm  26347  psercn  26352  pserdvlem2  26354  abelthlem3  26359  logtayl  26585  dvcxp1  26665  dvcncxp1  26668  logbmpt  26714  dmarea  26883  lgamgulmlem2  26956  lgamgulmlem5  26959  musum  27117  dchrptlem2  27192  dchrptlem3  27193  dchrpt  27194  lgsval  27228  lgsval4lem  27235  lgsneg  27248  lgsmod  27250  rpvmasum2  27439  padicfval  27543  ostth2  27564  ostth3  27565  ostth  27566  lmif  28748  islmib  28750  incistruhgr  29042  eucrct2eupth  30207  htthlem  30879  htth  30880  pjhfval  31358  hosmval  31697  hommval  31698  hodmval  31699  hfsmval  31700  hfmmval  31701  brafval  31905  kbfval  31914  mptprop  32654  indval  32809  psgnfzto1st  33060  fxpsubm  33127  fxpsubg  33128  fxpsubrg  33129  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnlem3  33197  elrgspnlem4  33198  elrgspn  33199  elrgspnsubrunlem1  33200  linds2eq  33331  elrspunidl  33378  elrspunsn  33379  evl1deg1  33524  evl1deg2  33525  evl1deg3  33526  lbsdiflsp0  33601  fedgmullem1  33604  fedgmullem2  33605  fedgmul  33606  evls1fldgencl  33644  fldextrspunlsplem  33647  fldextrspunlsp  33648  mdetpmtr1  33792  zar0ring  33847  ordtcnvNEW  33889  ordtrest2NEW  33892  xrhval  33987  esum2dlem  34061  ofceq  34066  itgeq12dv  34296  ballotlemfval  34460  vtsval  34607  lpadval  34646  ptpconn  35208  cvmliftlem15  35273  cvmlift2lem4  35281  cvmlift2  35291  snmlval  35306  snmlflim  35307  satf  35328  mrsubfval  35483  mrsubrn  35488  elmsubrn  35503  msubrn  35504  msubco  35506  faclim  35721  faclim2  35723  prodeq12sdv  36194  itgeq12sdv  36195  cbvsumdavw  36255  cbvproddavw  36256  cbvsumdavw2  36271  cbvproddavw2  36272  knoppcnlem1  36469  knoppcnlem6  36474  knoppcnlem7  36475  bj-evaleq  37048  csbrdgg  37305  curfv  37582  matunitlindflem2  37599  poimirlem5  37607  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem10  37612  poimirlem11  37613  poimirlem12  37614  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem18  37620  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem27  37629  voliunnfl  37646  itg2addnclem  37653  itg2addnclem3  37655  itg2addnc  37656  itg2gt0cn  37657  iblabsnclem  37665  iblmulc2nc  37667  ftc1anclem2  37676  ftc1anclem6  37680  ftc1anclem8  37682  ftc1anc  37683  ftc2nc  37684  upixp  37711  rrncmslem  37814  ismrer1  37820  tendoplcbv  40757  tendopl  40758  tendoicbv  40775  tendoi  40776  dihfval  41213  lcfl7N  41483  lcfrlem8  41531  lcfrlem9  41532  lcf1o  41533  hvmapval  41742  hdmap1fval  41778  hdmapffval  41808  hdmapfval  41809  hgmapffval  41867  hgmapfval  41868  lcmineqlem7  42011  lcmineqlem12  42016  aks6d1c6lem5  42153  rhmpsr  42528  evlsvval  42536  evlsvvval  42539  evlsbagval  42542  selvvvval  42561  evlselv  42563  fsuppind  42566  fsuppssindlem2  42568  fsuppssind  42569  mzpclval  42701  mzpcl2  42706  mzpexpmpt  42721  mzpsubst  42724  mzpcompact2lem  42727  rmxfval  42880  rmyfval  42881  aomclem8  43037  hbtlem1  43099  hbtlem7  43101  rfovfvd  43978  fsovrfovd  43985  fsovfvd  43986  fsovcnvlem  43989  dssmapfv2d  43994  dssmapnvod  43996  ntrneibex  44049  mnringmulrvald  44203  mnringmulrcld  44204  expgrowthi  44309  expgrowth  44311  binomcxplemdvsum  44331  addrval  44442  subrval  44443  mulvval  44444  fmulcl  45566  fmuldfeqlem1  45567  fprodcnlem  45584  fprodcn  45585  fnlimfv  45648  fnlimcnv  45652  fnlimfvre  45659  fnlimfvre2  45662  fnlimf  45663  fnlimabslt  45664  liminfval  45744  limsupresxr  45751  liminfresxr  45752  liminfvalxr  45768  fprodcncf  45885  dvnmptdivc  45923  dvnxpaek  45927  dvnmul  45928  dvmptfprod  45930  dvnprodlem1  45931  dvnprodlem2  45932  dvnprodlem3  45933  dvnprod  45934  stoweidlem2  45987  stoweidlem17  46002  stoweidlem19  46004  stoweidlem20  46005  stoweidlem43  46028  stoweidlem62  46047  stoweid  46048  dirkercncflem2  46089  fourierdlem112  46203  fourierdlem113  46204  etransclem1  46220  etransclem5  46224  etransclem17  46236  etransclem19  46238  etransclem22  46241  sge0val  46351  ovnlecvr  46543  ovncvrrp  46549  ovn0lem  46550  ovnsubaddlem1  46555  ovnsubadd  46557  hsphoif  46561  hsphoival  46564  hoidmv1lelem1  46576  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmv1le  46579  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem3  46582  hoidmvlelem4  46583  hoidmvlelem5  46584  hoidmvle  46585  ovnhoilem1  46586  ovnhoi  46588  hoidifhspval  46593  ovncvr2  46596  hoidifhspval2  46600  hspmbllem2  46612  hspmbllem3  46613  hspmbl  46614  ovnovollem1  46641  vonioolem2  46666  vonioo  46667  vonicclem2  46669  vonicc  46670  smflimlem4  46759  smflim  46762  smflim2  46791  smfsuplem2  46797  smfsup  46799  smfinf  46803  smflimsuplem2  46806  smflimsuplem5  46809  smflimsuplem7  46811  smflimsup  46813  cfsetsnfsetfo  47048  lincop  48397  1arymaptfv  48629  itcoval  48650  itcovalpc  48661  itcovalt2  48666  ackvalsuc1mpt  48667  ackval1  48670  fuco21  49325  prcofval  49367  aacllem  49790