Theorem mpteq2dv 5196

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

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

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 5165  df-mpt 5184

This theorem is referenced by:  ifmpt2v  7471  ofeqd  7635  mpocurryvald  8226  rdgeq1  8356  rdgeq2  8357  omv  8453  oev  8455  oieq1  9441  oieq2  9442  cantnflem1  9618  wunex2  10667  wuncval2  10676  rpnnen1  12918  seqof2  14001  relexpsucnnr  14967  relexp1g  14968  limsupval  15416  sumeq2w  15634  sumeq2ii  15635  cbvsum  15637  cbvsumv  15638  sumeq2sdv  15645  summo  15659  fsum  15662  fsumrlim  15753  fsumo1  15754  prodeq1  15849  prodeq2w  15852  prodeq2sdv  15865  prodmo  15878  fprod  15883  bpolylem  15990  rpnnen2lem1  16158  rpnnen2lem2  16159  1arithlem1  16870  vdwapval  16920  vdwlem6  16933  vdwlem8  16935  vdwlem9  16936  vdwlem10  16937  ramub1lem2  16974  ramcl  16976  sloteq  17129  prdsplusgval  17412  prdsmulrval  17414  prdsdsval  17417  prdsvscaval  17418  ismon  17671  fucco  17903  curf1  18162  curf2  18166  yonedalem4a  18212  smndex1gbas  18805  smndex1gid  18806  grplactfval  18949  galactghm  19310  pmtrval  19357  sylow1  19509  sylow2b  19529  sylow3lem5  19537  sylow3  19539  iscyg  19785  gsumzaddlem  19827  gsumzmhm  19843  ablfac2  19997  gsumdixp  20204  c0rhm  20419  c0rnghm  20420  zncyg  21434  phllmhm  21517  isphld  21539  frlmgsum  21657  frlmipval  21664  frlmphl  21666  uvcval  21670  fczpsrbag  21806  psrmulfval  21828  psrascl  21864  mvrval  21867  subrgmvr  21916  mplcoe1  21920  mplcoe3  21921  mplcoe5  21923  mplmon2  21944  subrgascl  21949  evlslem2  21962  evlslem3  21963  evlslem1  21965  mpfrcl  21968  evlsval  21969  evlsvar  21973  mpfind  21990  selvfval  21997  selvval  21998  mhpfval  22001  psdfval  22021  psdval  22022  psdmvr  22032  coe1fval  22066  pf1ind  22218  evl1gsumadd  22221  rhmmpl  22246  rhmply1vr1  22250  mamuval  22256  mamufv  22257  matgsum  22300  madetsumid  22324  mat1dimmul  22339  mvmulval  22406  mvmulfv  22407  mavmulfv  22409  1mavmul  22411  marepvval0  22429  mulmarep1gsum1  22436  mdetleib  22450  mdetleib2  22451  mdetfval1  22453  mdetleib1  22454  mdet0pr  22455  m1detdiag  22460  mdetralt  22471  mdetunilem9  22483  m2detleib  22494  smadiadetlem3  22531  mat2pmatmul  22594  decpmatmul  22635  decpmatmulsumfsupp  22636  pmatcollpw1  22639  monmatcollpw  22642  pmatcollpw3lem  22646  pmatcollpw3fi1lem2  22650  pm2mpval  22658  pm2mpfval  22659  mply1topmatval  22667  mp2pm2mplem1  22669  mp2pm2mplem3  22671  ptbasfi  23444  ptcnplem  23484  ptrescn  23502  cnmpt2k  23551  xkohmeo  23678  fmval  23806  fmf  23808  ptcmpg  23920  tmdmulg  23955  prdstmdd  23987  tsmspropd  23995  prdsxmslem2  24393  metdsval  24712  fsumcn  24737  expcn  24739  expcnOLD  24741  lebnumlem3  24838  pcoval  24887  pi1xfrcnv  24933  cphsscph  25127  rrxds  25269  rrxmval  25281  itg11  25568  mbfi1fseqlem2  25593  mbfi1fseqlem6  25597  mbfi1fseq  25598  mbfi1flimlem  25599  mbfmullem  25602  itg2const  25617  itg2mulc  25624  itg2monolem1  25627  itg2i1fseqle  25631  itg2i1fseq  25632  itg2addlem  25635  itg2cnlem1  25638  itg2cn  25640  isibl  25642  isibl2  25643  iblitg  25645  itgeq1  25650  itgz  25658  itgvallem  25662  itgvallem3  25663  iblcnlem1  25665  itgcnlem  25667  iblrelem  25668  iblposlem  25669  iblpos  25670  itgrevallem1  25672  itgposval  25673  iblss2  25683  itgss  25689  itgfsum  25704  iblabslem  25705  iblmulc2  25708  bddmulibl  25716  itgcn  25722  ellimc  25750  dvnfval  25800  cpnfval  25810  dvexp  25833  dvexp2  25834  dvmptfsum  25855  dvlipcn  25875  dvivthlem1  25889  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  dvfsumlem2  25909  dvfsumlem2OLD  25910  itgpowd  25933  elply2  26077  elplyr  26082  elplyd  26083  coeeu  26106  coelem  26107  coeeq  26108  plyco  26122  coe11  26134  coe1termlem  26139  dgrcolem1  26155  dvply2g  26168  dvply2gOLD  26169  elqaalem3  26205  eltayl  26243  tayl0  26245  taylthlem1  26257  taylthlem2  26258  taylthlem2OLD  26259  ulmcau  26280  ulmdvlem1  26285  ulmdvlem3  26287  mtest  26289  mtestbdd  26290  pserval  26295  pserulm  26307  psercn  26312  pserdvlem2  26314  abelthlem3  26319  logtayl  26545  dvcxp1  26625  dvcncxp1  26628  logbmpt  26674  dmarea  26843  lgamgulmlem2  26916  lgamgulmlem5  26919  musum  27077  dchrptlem2  27152  dchrptlem3  27153  dchrpt  27154  lgsval  27188  lgsval4lem  27195  lgsneg  27208  lgsmod  27210  rpvmasum2  27399  padicfval  27503  ostth2  27524  ostth3  27525  ostth  27526  lmif  28688  islmib  28690  incistruhgr  28982  eucrct2eupth  30147  htthlem  30819  htth  30820  pjhfval  31298  hosmval  31637  hommval  31638  hodmval  31639  hfsmval  31640  hfmmval  31641  brafval  31845  kbfval  31854  mptprop  32594  indval  32749  psgnfzto1st  33035  fxpsubm  33102  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnlem3  33168  elrgspnlem4  33169  elrgspn  33170  elrgspnsubrunlem1  33171  linds2eq  33325  elrspunidl  33372  elrspunsn  33373  evl1deg1  33518  evl1deg2  33519  evl1deg3  33520  lbsdiflsp0  33595  fedgmullem1  33598  fedgmullem2  33599  fedgmul  33600  evls1fldgencl  33638  fldextrspunlsplem  33641  fldextrspunlsp  33642  mdetpmtr1  33786  zar0ring  33841  ordtcnvNEW  33883  ordtrest2NEW  33886  xrhval  33981  esum2dlem  34055  ofceq  34060  itgeq12dv  34290  ballotlemfval  34454  vtsval  34601  lpadval  34640  ptpconn  35193  cvmliftlem15  35258  cvmlift2lem4  35266  cvmlift2  35276  snmlval  35291  snmlflim  35292  satf  35313  mrsubfval  35468  mrsubrn  35473  elmsubrn  35488  msubrn  35489  msubco  35491  faclim  35706  faclim2  35708  prodeq12sdv  36179  itgeq12sdv  36180  cbvsumdavw  36240  cbvproddavw  36241  cbvsumdavw2  36256  cbvproddavw2  36257  knoppcnlem1  36454  knoppcnlem6  36459  knoppcnlem7  36460  bj-evaleq  37033  csbrdgg  37290  curfv  37567  matunitlindflem2  37584  poimirlem5  37592  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  poimirlem10  37597  poimirlem11  37598  poimirlem12  37599  poimirlem15  37602  poimirlem16  37603  poimirlem17  37604  poimirlem18  37605  poimirlem19  37606  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem27  37614  voliunnfl  37631  itg2addnclem  37638  itg2addnclem3  37640  itg2addnc  37641  itg2gt0cn  37642  iblabsnclem  37650  iblmulc2nc  37652  ftc1anclem2  37661  ftc1anclem6  37665  ftc1anclem8  37667  ftc1anc  37668  ftc2nc  37669  upixp  37696  rrncmslem  37799  ismrer1  37805  tendoplcbv  40742  tendopl  40743  tendoicbv  40760  tendoi  40761  dihfval  41198  lcfl7N  41468  lcfrlem8  41516  lcfrlem9  41517  lcf1o  41518  hvmapval  41727  hdmap1fval  41763  hdmapffval  41793  hdmapfval  41794  hgmapffval  41852  hgmapfval  41853  lcmineqlem7  41996  lcmineqlem12  42001  aks6d1c6lem5  42138  rhmpsr  42513  evlsvval  42521  evlsvvval  42524  evlsbagval  42527  selvvvval  42546  evlselv  42548  fsuppind  42551  fsuppssindlem2  42553  fsuppssind  42554  mzpclval  42686  mzpcl2  42691  mzpexpmpt  42706  mzpsubst  42709  mzpcompact2lem  42712  rmxfval  42865  rmyfval  42866  aomclem8  43023  hbtlem1  43085  hbtlem7  43087  rfovfvd  43964  fsovrfovd  43971  fsovfvd  43972  fsovcnvlem  43975  dssmapfv2d  43980  dssmapnvod  43982  ntrneibex  44035  mnringmulrvald  44189  mnringmulrcld  44190  expgrowthi  44295  expgrowth  44297  binomcxplemdvsum  44317  addrval  44428  subrval  44429  mulvval  44430  fmulcl  45552  fmuldfeqlem1  45553  fprodcnlem  45570  fprodcn  45571  fnlimfv  45634  fnlimcnv  45638  fnlimfvre  45645  fnlimfvre2  45648  fnlimf  45649  fnlimabslt  45650  liminfval  45730  limsupresxr  45737  liminfresxr  45738  liminfvalxr  45754  fprodcncf  45871  dvnmptdivc  45909  dvnxpaek  45913  dvnmul  45914  dvmptfprod  45916  dvnprodlem1  45917  dvnprodlem2  45918  dvnprodlem3  45919  dvnprod  45920  stoweidlem2  45973  stoweidlem17  45988  stoweidlem19  45990  stoweidlem20  45991  stoweidlem43  46014  stoweidlem62  46033  stoweid  46034  dirkercncflem2  46075  fourierdlem112  46189  fourierdlem113  46190  etransclem1  46206  etransclem5  46210  etransclem17  46222  etransclem19  46224  etransclem22  46227  sge0val  46337  ovnlecvr  46529  ovncvrrp  46535  ovn0lem  46536  ovnsubaddlem1  46541  ovnsubadd  46543  hsphoif  46547  hsphoival  46550  hoidmv1lelem1  46562  hoidmv1lelem2  46563  hoidmv1lelem3  46564  hoidmv1le  46565  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem4  46569  hoidmvlelem5  46570  hoidmvle  46571  ovnhoilem1  46572  ovnhoi  46574  hoidifhspval  46579  ovncvr2  46582  hoidifhspval2  46586  hspmbllem2  46598  hspmbllem3  46599  hspmbl  46600  ovnovollem1  46627  vonioolem2  46652  vonioo  46653  vonicclem2  46655  vonicc  46656  smflimlem4  46745  smflim  46748  smflim2  46777  smfsuplem2  46783  smfsup  46785  smfinf  46789  smflimsuplem2  46792  smflimsuplem5  46795  smflimsuplem7  46797  smflimsup  46799  cfsetsnfsetfo  47034  lincop  48370  1arymaptfv  48602  itcoval  48623  itcovalpc  48634  itcovalt2  48639  ackvalsuc1mpt  48640  ackval1  48643  fuco21  49298  prcofval  49340  aacllem  49763