Theorem mpteq2dv 5251

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ↦ cmpt 5232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-opab 5212  df-mpt 5233

This theorem is referenced by:  ofeqd  7687  mpocurryvald  8276  rdgeq1  8432  rdgeq2  8433  omv  8533  oev  8535  oieq1  9537  oieq2  9538  cantnflem1  9714  wunex2  10763  wuncval2  10772  rpnnen1  13000  seqof2  14061  relexpsucnnr  15008  relexp1g  15009  limsupval  15454  sumeq2w  15674  sumeq2ii  15675  cbvsum  15677  summo  15699  fsum  15702  fsumrlim  15793  fsumo1  15794  prodeq2w  15892  prodmo  15916  fprod  15921  bpolylem  16028  rpnnen2lem1  16194  rpnnen2lem2  16195  1arithlem1  16895  vdwapval  16945  vdwlem6  16958  vdwlem8  16960  vdwlem9  16961  vdwlem10  16962  ramub1lem2  16999  ramcl  17001  sloteq  17155  prdsplusgval  17458  prdsmulrval  17460  prdsdsval  17463  prdsvscaval  17464  ismon  17719  fucco  17957  curf1  18220  curf2  18224  yonedalem4a  18270  smndex1gbas  18862  smndex1gid  18863  grplactfval  19005  galactghm  19371  pmtrval  19418  sylow1  19570  sylow2b  19590  sylow3lem5  19598  sylow3  19600  iscyg  19846  gsumzaddlem  19888  gsumzmhm  19904  ablfac2  20058  gsumdixp  20267  c0rhm  20483  c0rnghm  20484  zncyg  21499  phllmhm  21581  isphld  21603  frlmgsum  21723  frlmipval  21730  frlmphl  21732  uvcval  21736  fczpsrbag  21873  psrmulfval  21905  psrascl  21941  mvrval  21944  subrgmvr  21993  mplcoe1  21997  mplcoe3  21998  mplcoe5  22000  mplmon2  22027  subrgascl  22032  evlslem2  22047  evlslem3  22048  evlslem1  22050  mpfrcl  22053  evlsval  22054  evlsvar  22058  mpfind  22075  selvfval  22082  selvval  22083  mhpfval  22086  psdfval  22105  psdval  22106  coe1fval  22148  pf1ind  22299  evl1gsumadd  22302  rhmmpl  22327  rhmply1vr1  22331  mamuval  22337  mamufv  22338  matgsum  22383  madetsumid  22407  mat1dimmul  22422  mvmulval  22489  mvmulfv  22490  mavmulfv  22492  1mavmul  22494  marepvval0  22512  mulmarep1gsum1  22519  mdetleib  22533  mdetleib2  22534  mdetfval1  22536  mdetleib1  22537  mdet0pr  22538  m1detdiag  22543  mdetralt  22554  mdetunilem9  22566  m2detleib  22577  smadiadetlem3  22614  mat2pmatmul  22677  decpmatmul  22718  decpmatmulsumfsupp  22719  pmatcollpw1  22722  monmatcollpw  22725  pmatcollpw3lem  22729  pmatcollpw3fi1lem2  22733  pm2mpval  22741  pm2mpfval  22742  mply1topmatval  22750  mp2pm2mplem1  22752  mp2pm2mplem3  22754  ptbasfi  23529  ptcnplem  23569  ptrescn  23587  cnmpt2k  23636  xkohmeo  23763  fmval  23891  fmf  23893  ptcmpg  24005  tmdmulg  24040  prdstmdd  24072  tsmspropd  24080  prdsxmslem2  24482  metdsval  24807  fsumcn  24832  expcn  24834  expcnOLD  24836  lebnumlem3  24933  pcoval  24982  pi1xfrcnv  25028  cphsscph  25223  rrxds  25365  rrxmval  25377  itg11  25664  mbfi1fseqlem2  25690  mbfi1fseqlem6  25694  mbfi1fseq  25695  mbfi1flimlem  25696  mbfmullem  25699  itg2const  25714  itg2mulc  25721  itg2monolem1  25724  itg2i1fseqle  25728  itg2i1fseq  25729  itg2addlem  25732  itg2cnlem1  25735  itg2cn  25737  isibl  25739  isibl2  25740  iblitg  25742  itgz  25754  itgvallem  25758  itgvallem3  25759  iblcnlem1  25761  itgcnlem  25763  iblrelem  25764  iblposlem  25765  iblpos  25766  itgrevallem1  25768  itgposval  25769  iblss2  25779  itgss  25785  itgfsum  25800  iblabslem  25801  iblmulc2  25804  bddmulibl  25812  itgcn  25818  ellimc  25846  dvnfval  25896  cpnfval  25906  dvexp  25929  dvexp2  25930  dvmptfsum  25951  dvlipcn  25971  dvivthlem1  25985  dvfsumle  25998  dvfsumleOLD  25999  dvfsumabs  26001  dvfsumlem2  26005  dvfsumlem2OLD  26006  itgpowd  26029  elply2  26175  elplyr  26180  elplyd  26181  coeeu  26204  coelem  26205  coeeq  26206  plyco  26220  coe11  26232  coe1termlem  26237  dgrcolem1  26253  dvply2g  26264  dvply2gOLD  26265  elqaalem3  26301  eltayl  26339  tayl0  26341  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulmcau  26376  ulmdvlem1  26381  ulmdvlem3  26383  mtest  26385  mtestbdd  26386  pserval  26391  pserulm  26403  psercn  26408  pserdvlem2  26410  abelthlem3  26415  logtayl  26639  dvcxp1  26719  dvcncxp1  26722  logbmpt  26765  dmarea  26934  lgamgulmlem2  27007  lgamgulmlem5  27010  musum  27168  dchrptlem2  27243  dchrptlem3  27244  dchrpt  27245  lgsval  27279  lgsval4lem  27286  lgsneg  27299  lgsmod  27301  rpvmasum2  27490  padicfval  27594  ostth2  27615  ostth3  27616  ostth  27617  lmif  28661  islmib  28663  incistruhgr  28964  eucrct2eupth  30127  htthlem  30799  htth  30800  pjhfval  31278  hosmval  31617  hommval  31618  hodmval  31619  hfsmval  31620  hfmmval  31621  brafval  31825  kbfval  31834  mptprop  32560  psgnfzto1st  32918  linds2eq  33193  elrspunidl  33240  elrspunsn  33241  evl1deg1  33387  lbsdiflsp0  33455  fedgmullem1  33458  fedgmullem2  33459  fedgmul  33460  evls1fldgencl  33489  mdetpmtr1  33555  zar0ring  33610  ordtcnvNEW  33652  ordtrest2NEW  33655  xrhval  33750  indval  33763  esum2dlem  33842  ofceq  33847  itgeq12dv  34077  ballotlemfval  34240  vtsval  34400  lpadval  34439  ptpconn  34974  cvmliftlem15  35039  cvmlift2lem4  35047  cvmlift2  35057  snmlval  35072  snmlflim  35073  satf  35094  mrsubfval  35249  mrsubrn  35254  elmsubrn  35269  msubrn  35270  msubco  35272  faclim  35471  faclim2  35473  knoppcnlem1  36099  knoppcnlem6  36104  knoppcnlem7  36105  bj-evaleq  36682  csbrdgg  36939  curfv  37204  matunitlindflem2  37221  poimirlem5  37229  poimirlem6  37230  poimirlem7  37231  poimirlem8  37232  poimirlem10  37234  poimirlem11  37235  poimirlem12  37236  poimirlem15  37239  poimirlem16  37240  poimirlem17  37241  poimirlem18  37242  poimirlem19  37243  poimirlem20  37244  poimirlem21  37245  poimirlem22  37246  poimirlem27  37251  voliunnfl  37268  itg2addnclem  37275  itg2addnclem3  37277  itg2addnc  37278  itg2gt0cn  37279  iblabsnclem  37287  iblmulc2nc  37289  ftc1anclem2  37298  ftc1anclem6  37302  ftc1anclem8  37304  ftc1anc  37305  ftc2nc  37306  upixp  37333  rrncmslem  37436  ismrer1  37442  tendoplcbv  40378  tendopl  40379  tendoicbv  40396  tendoi  40397  dihfval  40834  lcfl7N  41104  lcfrlem8  41152  lcfrlem9  41153  lcf1o  41154  hvmapval  41363  hdmap1fval  41399  hdmapffval  41429  hdmapfval  41430  hgmapffval  41488  hgmapfval  41489  lcmineqlem7  41638  lcmineqlem12  41643  aks6d1c6lem5  41780  rhmpsr  41920  evlsvval  41928  evlsvvval  41931  evlsbagval  41934  selvvvval  41953  evlselv  41955  fsuppind  41958  fsuppssindlem2  41960  fsuppssind  41961  mzpclval  42287  mzpcl2  42292  mzpexpmpt  42307  mzpsubst  42310  mzpcompact2lem  42313  rmxfval  42466  rmyfval  42467  aomclem8  42627  hbtlem1  42689  hbtlem7  42691  rfovfvd  43574  fsovrfovd  43581  fsovfvd  43582  fsovcnvlem  43585  dssmapfv2d  43590  dssmapnvod  43592  ntrneibex  43645  mnringmulrvald  43806  mnringmulrcld  43807  expgrowthi  43912  expgrowth  43914  binomcxplemdvsum  43934  addrval  44045  subrval  44046  mulvval  44047  fmulcl  45107  fmuldfeqlem1  45108  fprodcnlem  45125  fprodcn  45126  fnlimfv  45189  fnlimcnv  45193  fnlimfvre  45200  fnlimfvre2  45203  fnlimf  45204  fnlimabslt  45205  liminfval  45285  limsupresxr  45292  liminfresxr  45293  liminfvalxr  45309  fprodcncf  45426  dvnmptdivc  45464  dvnxpaek  45468  dvnmul  45469  dvmptfprod  45471  dvnprodlem1  45472  dvnprodlem2  45473  dvnprodlem3  45474  dvnprod  45475  stoweidlem2  45528  stoweidlem17  45543  stoweidlem19  45545  stoweidlem20  45546  stoweidlem43  45569  stoweidlem62  45588  stoweid  45589  dirkercncflem2  45630  fourierdlem112  45744  fourierdlem113  45745  etransclem1  45761  etransclem5  45765  etransclem17  45777  etransclem19  45779  etransclem22  45782  sge0val  45892  ovnlecvr  46084  ovncvrrp  46090  ovn0lem  46091  ovnsubaddlem1  46096  ovnsubadd  46098  hsphoif  46102  hsphoival  46105  hoidmv1lelem1  46117  hoidmv1lelem2  46118  hoidmv1lelem3  46119  hoidmv1le  46120  hoidmvlelem1  46121  hoidmvlelem2  46122  hoidmvlelem3  46123  hoidmvlelem4  46124  hoidmvlelem5  46125  hoidmvle  46126  ovnhoilem1  46127  ovnhoi  46129  hoidifhspval  46134  ovncvr2  46137  hoidifhspval2  46141  hspmbllem2  46153  hspmbllem3  46154  hspmbl  46155  ovnovollem1  46182  vonioolem2  46207  vonioo  46208  vonicclem2  46210  vonicc  46211  smflimlem4  46300  smflim  46303  smflim2  46332  smfsuplem2  46338  smfsup  46340  smfinf  46344  smflimsuplem2  46347  smflimsuplem5  46350  smflimsuplem7  46352  smflimsup  46354  cfsetsnfsetfo  46580  lincop  47662  1arymaptfv  47899  itcoval  47920  itcovalpc  47931  itcovalt2  47936  ackvalsuc1mpt  47937  ackval1  47940  aacllem  48420