Theorem mpteq2dv 5172

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-mpt 5154

This theorem is referenced by:  ofeqd  7513  mpocurryvald  8057  rdgeq1  8213  rdgeq2  8214  omv  8304  oev  8306  oieq1  9201  oieq2  9202  cantnflem1  9377  trpredeq1  9398  trpredeq2  9399  wunex2  10425  wuncval2  10434  rpnnen1  12652  seqof2  13709  relexpsucnnr  14664  relexp1g  14665  limsupval  15111  sumeq2w  15332  sumeq2ii  15333  cbvsum  15335  summo  15357  fsum  15360  fsumrlim  15451  fsumo1  15452  prodeq2w  15550  prodmo  15574  fprod  15579  bpolylem  15686  rpnnen2lem1  15851  rpnnen2lem2  15852  1arithlem1  16552  vdwapval  16602  vdwlem6  16615  vdwlem8  16617  vdwlem9  16618  vdwlem10  16619  ramub1lem2  16656  ramcl  16658  sloteq  16812  prdsplusgval  17101  prdsmulrval  17103  prdsdsval  17106  prdsvscaval  17107  ismon  17362  fucco  17596  curf1  17859  curf2  17863  yonedalem4a  17909  smndex1gbas  18456  smndex1gid  18457  grplactfval  18591  galactghm  18927  pmtrval  18974  sylow1  19123  sylow2b  19143  sylow3lem5  19151  sylow3  19153  iscyg  19394  gsumzaddlem  19437  gsumzmhm  19453  ablfac2  19607  gsumdixp  19763  zncyg  20668  phllmhm  20749  isphld  20771  frlmgsum  20889  frlmipval  20896  frlmphl  20898  uvcval  20902  fczpsrbag  21036  psrmulfval  21064  mvrval  21100  subrgmvr  21144  mplcoe1  21148  mplcoe3  21149  mplcoe5  21151  mplmon2  21179  subrgascl  21184  evlslem2  21199  evlslem3  21200  evlslem1  21202  mpfrcl  21205  evlsval  21206  evlsvar  21210  mpfind  21227  selvfval  21237  selvval  21238  mhpfval  21239  coe1fval  21286  pf1ind  21431  evl1gsumadd  21434  mamuval  21445  mamufv  21446  matgsum  21494  madetsumid  21518  mat1dimmul  21533  mvmulval  21600  mvmulfv  21601  mavmulfv  21603  1mavmul  21605  marepvval0  21623  mulmarep1gsum1  21630  mdetleib  21644  mdetleib2  21645  mdetfval1  21647  mdetleib1  21648  mdet0pr  21649  m1detdiag  21654  mdetralt  21665  mdetunilem9  21677  m2detleib  21688  smadiadetlem3  21725  mat2pmatmul  21788  decpmatmul  21829  decpmatmulsumfsupp  21830  pmatcollpw1  21833  monmatcollpw  21836  pmatcollpw3lem  21840  pmatcollpw3fi1lem2  21844  pm2mpval  21852  pm2mpfval  21853  mply1topmatval  21861  mp2pm2mplem1  21863  mp2pm2mplem3  21865  ptbasfi  22640  ptcnplem  22680  ptrescn  22698  cnmpt2k  22747  xkohmeo  22874  fmval  23002  fmf  23004  ptcmpg  23116  tmdmulg  23151  prdstmdd  23183  tsmspropd  23191  prdsxmslem2  23591  metdsval  23916  fsumcn  23939  expcn  23941  lebnumlem3  24032  pcoval  24080  pi1xfrcnv  24126  cphsscph  24320  rrxds  24462  rrxmval  24474  itg11  24760  mbfi1fseqlem2  24786  mbfi1fseqlem6  24790  mbfi1fseq  24791  mbfi1flimlem  24792  mbfmullem  24795  itg2const  24810  itg2mulc  24817  itg2monolem1  24820  itg2i1fseqle  24824  itg2i1fseq  24825  itg2addlem  24828  itg2cnlem1  24831  itg2cn  24833  isibl  24835  isibl2  24836  iblitg  24838  itgz  24850  itgvallem  24854  itgvallem3  24855  iblcnlem1  24857  itgcnlem  24859  iblrelem  24860  iblposlem  24861  iblpos  24862  itgrevallem1  24864  itgposval  24865  iblss2  24875  itgss  24881  itgfsum  24896  iblabslem  24897  iblmulc2  24900  bddmulibl  24908  itgcn  24914  ellimc  24942  dvnfval  24991  cpnfval  25001  dvexp  25022  dvexp2  25023  dvmptfsum  25044  dvlipcn  25063  dvivthlem1  25077  dvfsumle  25090  dvfsumabs  25092  dvfsumlem2  25096  itgpowd  25119  elply2  25262  elplyr  25267  elplyd  25268  coeeu  25291  coelem  25292  coeeq  25293  plyco  25307  coe11  25319  coe1termlem  25324  dgrcolem1  25339  dvply2g  25350  elqaalem3  25386  eltayl  25424  tayl0  25426  taylthlem1  25437  taylthlem2  25438  ulmcau  25459  ulmdvlem1  25464  ulmdvlem3  25466  mtest  25468  mtestbdd  25469  pserval  25474  pserulm  25486  psercn  25490  pserdvlem2  25492  abelthlem3  25497  logtayl  25720  dvcxp1  25798  dvcncxp1  25801  logbmpt  25843  dmarea  26012  lgamgulmlem2  26084  lgamgulmlem5  26087  musum  26245  dchrptlem2  26318  dchrptlem3  26319  dchrpt  26320  lgsval  26354  lgsval4lem  26361  lgsneg  26374  lgsmod  26376  rpvmasum2  26565  padicfval  26669  ostth2  26690  ostth3  26691  ostth  26692  lmif  27050  islmib  27052  incistruhgr  27352  eucrct2eupth  28510  htthlem  29180  htth  29181  pjhfval  29659  hosmval  29998  hommval  29999  hodmval  30000  hfsmval  30001  hfmmval  30002  brafval  30206  kbfval  30215  mptprop  30933  psgnfzto1st  31274  linds2eq  31477  elrspunidl  31508  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  mdetpmtr1  31675  zar0ring  31730  ordtcnvNEW  31772  ordtrest2NEW  31775  xrhval  31868  indval  31881  esum2dlem  31960  ofceq  31965  itgeq12dv  32193  ballotlemfval  32356  vtsval  32517  lpadval  32556  ptpconn  33095  cvmliftlem15  33160  cvmlift2lem4  33168  cvmlift2  33178  snmlval  33193  snmlflim  33194  satf  33215  mrsubfval  33370  mrsubrn  33375  elmsubrn  33390  msubrn  33391  msubco  33393  faclim  33618  faclim2  33620  knoppcnlem1  34600  knoppcnlem6  34605  knoppcnlem7  34606  bj-evaleq  35170  csbrdgg  35427  curfv  35684  matunitlindflem2  35701  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem27  35731  voliunnfl  35748  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  iblabsnclem  35767  iblmulc2nc  35769  ftc1anclem2  35778  ftc1anclem6  35782  ftc1anclem8  35784  ftc1anc  35785  ftc2nc  35786  upixp  35814  rrncmslem  35917  ismrer1  35923  tendoplcbv  38716  tendopl  38717  tendoicbv  38734  tendoi  38735  dihfval  39172  lcfl7N  39442  lcfrlem8  39490  lcfrlem9  39491  lcf1o  39492  hvmapval  39701  hdmap1fval  39737  hdmapffval  39767  hdmapfval  39768  hgmapffval  39826  hgmapfval  39827  lcmineqlem7  39971  lcmineqlem12  39976  evlsbagval  40198  fsuppind  40202  fsuppssindlem2  40204  fsuppssind  40205  mzpclval  40463  mzpcl2  40468  mzpexpmpt  40483  mzpsubst  40486  mzpcompact2lem  40489  rmxfval  40642  rmyfval  40643  aomclem8  40802  hbtlem1  40864  hbtlem7  40866  rfovfvd  41499  fsovrfovd  41506  fsovfvd  41507  fsovcnvlem  41510  dssmapfv2d  41515  dssmapnvod  41517  ntrneibex  41572  mnringmulrvald  41734  mnringmulrcld  41735  expgrowthi  41840  expgrowth  41842  binomcxplemdvsum  41862  addrval  41973  subrval  41974  mulvval  41975  fmulcl  43012  fmuldfeqlem1  43013  fprodcnlem  43030  fprodcn  43031  fnlimfv  43094  fnlimcnv  43098  fnlimfvre  43105  fnlimfvre2  43108  fnlimf  43109  fnlimabslt  43110  liminfval  43190  limsupresxr  43197  liminfresxr  43198  liminfvalxr  43214  fprodcncf  43331  dvnmptdivc  43369  dvnxpaek  43373  dvnmul  43374  dvmptfprod  43376  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  dvnprod  43380  stoweidlem2  43433  stoweidlem17  43448  stoweidlem19  43450  stoweidlem20  43451  stoweidlem43  43474  stoweidlem62  43493  stoweid  43494  dirkercncflem2  43535  fourierdlem112  43649  fourierdlem113  43650  etransclem1  43666  etransclem5  43670  etransclem17  43682  etransclem19  43684  etransclem22  43687  sge0val  43794  ovnlecvr  43986  ovncvrrp  43992  ovn0lem  43993  ovnsubaddlem1  43998  ovnsubadd  44000  hsphoif  44004  hsphoival  44007  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvlelem5  44027  hoidmvle  44028  ovnhoilem1  44029  ovnhoi  44031  hoidifhspval  44036  ovncvr2  44039  hoidifhspval2  44043  hspmbllem2  44055  hspmbllem3  44056  hspmbl  44057  ovnovollem1  44084  vonioolem2  44109  vonioo  44110  vonicclem2  44112  vonicc  44113  smflimlem4  44196  smflim  44199  smflim2  44226  smfsuplem2  44232  smfsup  44234  smfinf  44238  smflimsuplem2  44241  smflimsuplem5  44244  smflimsuplem7  44246  smflimsup  44248  cfsetsnfsetfo  44441  c0rhm  45358  c0rnghm  45359  lincop  45637  1arymaptfv  45874  itcoval  45895  itcovalpc  45906  itcovalt2  45911  ackvalsuc1mpt  45912  ackval1  45915  aacllem  46391