Theorem mpteq2dv 5162

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   ↦ cmpt 5146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-opab 5129  df-mpt 5147

This theorem is referenced by:  ofeq  7411  mpocurryvald  7936  rdgeq1  8047  rdgeq2  8048  omv  8137  oev  8139  oieq1  8976  oieq2  8977  cantnflem1  9152  wunex2  10160  wuncval2  10169  rpnnen1  12383  seqof2  13429  relexpsucnnr  14384  relexp1g  14385  limsupval  14831  sumeq2w  15049  sumeq2ii  15050  cbvsum  15052  summo  15074  fsum  15077  fsumrlim  15166  fsumo1  15167  prodeq2w  15266  prodmo  15290  fprod  15295  bpolylem  15402  rpnnen2lem1  15567  rpnnen2lem2  15568  1arithlem1  16259  vdwapval  16309  vdwlem6  16322  vdwlem8  16324  vdwlem9  16325  vdwlem10  16326  ramub1lem2  16363  ramcl  16365  sloteq  16488  prdsplusgval  16746  prdsmulrval  16748  prdsdsval  16751  prdsvscaval  16752  ismon  17003  fucco  17232  curf1  17475  curf2  17479  yonedalem4a  17525  smndex1gbas  18067  smndex1gid  18068  grplactfval  18200  galactghm  18532  pmtrval  18579  sylow1  18728  sylow2b  18748  sylow3lem5  18756  sylow3  18758  iscyg  18998  gsumzaddlem  19041  gsumzmhm  19057  ablfac2  19211  gsumdixp  19359  fczpsrbag  20147  psrmulfval  20165  mvrval  20201  subrgmvr  20242  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  mplmon2  20273  subrgascl  20278  evlslem2  20292  evlslem3  20293  evlslem1  20295  mpfrcl  20298  evlsval  20299  evlsvar  20303  mpfind  20320  selvfval  20330  selvval  20331  mhpfval  20332  coe1fval  20373  pf1ind  20518  evl1gsumadd  20521  zncyg  20695  phllmhm  20776  isphld  20798  frlmgsum  20916  frlmipval  20923  frlmphl  20925  uvcval  20929  mamuval  20997  mamufv  20998  matgsum  21046  madetsumid  21070  mat1dimmul  21085  mvmulval  21152  mvmulfv  21153  mavmulfv  21155  1mavmul  21157  marepvval0  21175  mulmarep1gsum1  21182  mdetleib  21196  mdetleib2  21197  mdetfval1  21199  mdetleib1  21200  mdet0pr  21201  m1detdiag  21206  mdetralt  21217  mdetunilem9  21229  m2detleib  21240  smadiadetlem3  21277  mat2pmatmul  21339  decpmatmul  21380  decpmatmulsumfsupp  21381  pmatcollpw1  21384  monmatcollpw  21387  pmatcollpw3lem  21391  pmatcollpw3fi1lem2  21395  pm2mpval  21403  pm2mpfval  21404  mply1topmatval  21412  mp2pm2mplem1  21414  mp2pm2mplem3  21416  ptbasfi  22189  ptcnplem  22229  ptrescn  22247  cnmpt2k  22296  xkohmeo  22423  fmval  22551  fmf  22553  ptcmpg  22665  tmdmulg  22700  prdstmdd  22732  tsmspropd  22740  prdsxmslem2  23139  metdsval  23455  fsumcn  23478  expcn  23480  lebnumlem3  23567  pcoval  23615  pi1xfrcnv  23661  cphsscph  23854  rrxds  23996  rrxmval  24008  itg11  24292  mbfi1fseqlem2  24317  mbfi1fseqlem6  24321  mbfi1fseq  24322  mbfi1flimlem  24323  mbfmullem  24326  itg2const  24341  itg2mulc  24348  itg2monolem1  24351  itg2i1fseqle  24355  itg2i1fseq  24356  itg2addlem  24359  itg2cnlem1  24362  itg2cn  24364  isibl  24366  isibl2  24367  iblitg  24369  itgz  24381  itgvallem  24385  itgvallem3  24386  iblcnlem1  24388  itgcnlem  24390  iblrelem  24391  iblposlem  24392  iblpos  24393  itgrevallem1  24395  itgposval  24396  iblss2  24406  itgss  24412  itgfsum  24427  iblabslem  24428  iblmulc2  24431  bddmulibl  24439  itgcn  24443  ellimc  24471  dvnfval  24519  cpnfval  24529  dvexp  24550  dvexp2  24551  dvmptfsum  24572  dvlipcn  24591  dvivthlem1  24605  dvfsumle  24618  dvfsumabs  24620  dvfsumlem2  24624  elply2  24786  elplyr  24791  elplyd  24792  coeeu  24815  coelem  24816  coeeq  24817  plyco  24831  coe11  24843  coe1termlem  24848  dgrcolem1  24863  dvply2g  24874  elqaalem3  24910  eltayl  24948  tayl0  24950  taylthlem1  24961  taylthlem2  24962  ulmcau  24983  ulmdvlem1  24988  ulmdvlem3  24990  mtest  24992  mtestbdd  24993  pserval  24998  pserulm  25010  psercn  25014  pserdvlem2  25016  abelthlem3  25021  logtayl  25243  dvcxp1  25321  dvcncxp1  25324  logbmpt  25366  dmarea  25535  lgamgulmlem2  25607  lgamgulmlem5  25610  musum  25768  dchrptlem2  25841  dchrptlem3  25842  dchrpt  25843  lgsval  25877  lgsval4lem  25884  lgsneg  25897  lgsmod  25899  rpvmasum2  26088  padicfval  26192  ostth2  26213  ostth3  26214  ostth  26215  lmif  26571  islmib  26573  incistruhgr  26864  eucrct2eupth  28024  htthlem  28694  htth  28695  pjhfval  29173  hosmval  29512  hommval  29513  hodmval  29514  hfsmval  29515  hfmmval  29516  brafval  29720  kbfval  29729  mptprop  30434  psgnfzto1st  30747  linds2eq  30941  lbsdiflsp0  31022  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  mdetpmtr1  31088  ordtcnvNEW  31163  ordtrest2NEW  31166  xrhval  31259  indval  31272  esum2dlem  31351  ofceq  31356  itgeq12dv  31584  ballotlemfval  31747  vtsval  31908  lpadval  31947  ptpconn  32480  cvmliftlem15  32545  cvmlift2lem4  32553  cvmlift2  32563  snmlval  32578  snmlflim  32579  satf  32600  mrsubfval  32755  mrsubrn  32760  elmsubrn  32775  msubrn  32776  msubco  32778  faclim  32978  faclim2  32980  trpredeq1  33059  trpredeq2  33060  knoppcnlem1  33832  knoppcnlem6  33837  knoppcnlem7  33838  bj-evaleq  34366  csbrdgg  34613  curfv  34887  matunitlindflem2  34904  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem27  34934  voliunnfl  34951  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  itg2gt0cn  34962  iblabsnclem  34970  iblmulc2nc  34972  ftc1anclem2  34983  ftc1anclem6  34987  ftc1anclem8  34989  ftc1anc  34990  ftc2nc  34991  upixp  35019  rrncmslem  35125  ismrer1  35131  tendoplcbv  37926  tendopl  37927  tendoicbv  37944  tendoi  37945  dihfval  38382  lcfl7N  38652  lcfrlem8  38700  lcfrlem9  38701  lcf1o  38702  hvmapval  38911  hdmap1fval  38947  hdmapffval  38977  hdmapfval  38978  hgmapffval  39036  hgmapfval  39037  mzpclval  39371  mzpcl2  39376  mzpexpmpt  39391  mzpsubst  39394  mzpcompact2lem  39397  rmxfval  39550  rmyfval  39551  aomclem8  39710  hbtlem1  39772  hbtlem7  39774  itgpowd  39870  rfovfvd  40397  fsovrfovd  40404  fsovfvd  40405  fsovcnvlem  40408  dssmapfv2d  40413  dssmapnvod  40415  ntrneibex  40472  expgrowthi  40714  expgrowth  40716  binomcxplemdvsum  40736  addrval  40847  subrval  40848  mulvval  40849  fmulcl  41911  fmuldfeqlem1  41912  fprodcnlem  41929  fprodcn  41930  fnlimfv  41993  fnlimcnv  41997  fnlimfvre  42004  fnlimfvre2  42007  fnlimf  42008  fnlimabslt  42009  liminfval  42089  limsupresxr  42096  liminfresxr  42097  liminfvalxr  42113  fprodcncf  42233  dvnmptdivc  42272  dvnxpaek  42276  dvnmul  42277  dvmptfprod  42279  dvnprodlem1  42280  dvnprodlem2  42281  dvnprodlem3  42282  dvnprod  42283  stoweidlem2  42336  stoweidlem17  42351  stoweidlem19  42353  stoweidlem20  42354  stoweidlem43  42377  stoweidlem62  42396  stoweid  42397  dirkercncflem2  42438  fourierdlem112  42552  fourierdlem113  42553  etransclem1  42569  etransclem5  42573  etransclem17  42585  etransclem19  42587  etransclem22  42590  sge0val  42697  ovnlecvr  42889  ovncvrrp  42895  ovn0lem  42896  ovnsubaddlem1  42901  ovnsubadd  42903  hsphoif  42907  hsphoival  42910  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  hoidmvlelem5  42930  hoidmvle  42931  ovnhoilem1  42932  ovnhoi  42934  hoidifhspval  42939  ovncvr2  42942  hoidifhspval2  42946  hspmbllem2  42958  hspmbllem3  42959  hspmbl  42960  ovnovollem1  42987  vonioolem2  43012  vonioo  43013  vonicclem2  43015  vonicc  43016  smflimlem4  43099  smflim  43102  smflim2  43129  smfsuplem2  43135  smfsup  43137  smfinf  43141  smflimsuplem2  43144  smflimsuplem5  43147  smflimsuplem7  43149  smflimsup  43151  c0rhm  44232  c0rnghm  44233  lincop  44512  aacllem  44951