Theorem mpteq2dv 5250

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5211  df-mpt 5232

This theorem is referenced by:  ofeqd  7674  mpocurryvald  8257  rdgeq1  8413  rdgeq2  8414  omv  8514  oev  8516  oieq1  9509  oieq2  9510  cantnflem1  9686  wunex2  10735  wuncval2  10744  rpnnen1  12971  seqof2  14030  relexpsucnnr  14976  relexp1g  14977  limsupval  15422  sumeq2w  15642  sumeq2ii  15643  cbvsum  15645  summo  15667  fsum  15670  fsumrlim  15761  fsumo1  15762  prodeq2w  15860  prodmo  15884  fprod  15889  bpolylem  15996  rpnnen2lem1  16161  rpnnen2lem2  16162  1arithlem1  16860  vdwapval  16910  vdwlem6  16923  vdwlem8  16925  vdwlem9  16926  vdwlem10  16927  ramub1lem2  16964  ramcl  16966  sloteq  17120  prdsplusgval  17423  prdsmulrval  17425  prdsdsval  17428  prdsvscaval  17429  ismon  17684  fucco  17919  curf1  18182  curf2  18186  yonedalem4a  18232  smndex1gbas  18819  smndex1gid  18820  grplactfval  18960  galactghm  19313  pmtrval  19360  sylow1  19512  sylow2b  19532  sylow3lem5  19540  sylow3  19542  iscyg  19788  gsumzaddlem  19830  gsumzmhm  19846  ablfac2  20000  gsumdixp  20207  c0rhm  20423  c0rnghm  20424  zncyg  21323  phllmhm  21404  isphld  21426  frlmgsum  21546  frlmipval  21553  frlmphl  21555  uvcval  21559  fczpsrbag  21695  psrmulfval  21723  mvrval  21760  subrgmvr  21807  mplcoe1  21811  mplcoe3  21812  mplcoe5  21814  mplmon2  21841  subrgascl  21846  evlslem2  21861  evlslem3  21862  evlslem1  21864  mpfrcl  21867  evlsval  21868  evlsvar  21872  mpfind  21889  selvfval  21899  selvval  21900  mhpfval  21901  coe1fval  21948  pf1ind  22094  evl1gsumadd  22097  mamuval  22108  mamufv  22109  matgsum  22159  madetsumid  22183  mat1dimmul  22198  mvmulval  22265  mvmulfv  22266  mavmulfv  22268  1mavmul  22270  marepvval0  22288  mulmarep1gsum1  22295  mdetleib  22309  mdetleib2  22310  mdetfval1  22312  mdetleib1  22313  mdet0pr  22314  m1detdiag  22319  mdetralt  22330  mdetunilem9  22342  m2detleib  22353  smadiadetlem3  22390  mat2pmatmul  22453  decpmatmul  22494  decpmatmulsumfsupp  22495  pmatcollpw1  22498  monmatcollpw  22501  pmatcollpw3lem  22505  pmatcollpw3fi1lem2  22509  pm2mpval  22517  pm2mpfval  22518  mply1topmatval  22526  mp2pm2mplem1  22528  mp2pm2mplem3  22530  ptbasfi  23305  ptcnplem  23345  ptrescn  23363  cnmpt2k  23412  xkohmeo  23539  fmval  23667  fmf  23669  ptcmpg  23781  tmdmulg  23816  prdstmdd  23848  tsmspropd  23856  prdsxmslem2  24258  metdsval  24583  fsumcn  24608  expcn  24610  expcnOLD  24612  lebnumlem3  24703  pcoval  24751  pi1xfrcnv  24797  cphsscph  24992  rrxds  25134  rrxmval  25146  itg11  25432  mbfi1fseqlem2  25458  mbfi1fseqlem6  25462  mbfi1fseq  25463  mbfi1flimlem  25464  mbfmullem  25467  itg2const  25482  itg2mulc  25489  itg2monolem1  25492  itg2i1fseqle  25496  itg2i1fseq  25497  itg2addlem  25500  itg2cnlem1  25503  itg2cn  25505  isibl  25507  isibl2  25508  iblitg  25510  itgz  25522  itgvallem  25526  itgvallem3  25527  iblcnlem1  25529  itgcnlem  25531  iblrelem  25532  iblposlem  25533  iblpos  25534  itgrevallem1  25536  itgposval  25537  iblss2  25547  itgss  25553  itgfsum  25568  iblabslem  25569  iblmulc2  25572  bddmulibl  25580  itgcn  25586  ellimc  25614  dvnfval  25663  cpnfval  25673  dvexp  25694  dvexp2  25695  dvmptfsum  25716  dvlipcn  25735  dvivthlem1  25749  dvfsumle  25762  dvfsumabs  25764  dvfsumlem2  25768  itgpowd  25791  elply2  25934  elplyr  25939  elplyd  25940  coeeu  25963  coelem  25964  coeeq  25965  plyco  25979  coe11  25991  coe1termlem  25996  dgrcolem1  26011  dvply2g  26022  elqaalem3  26058  eltayl  26096  tayl0  26098  taylthlem1  26109  taylthlem2  26110  ulmcau  26131  ulmdvlem1  26136  ulmdvlem3  26138  mtest  26140  mtestbdd  26141  pserval  26146  pserulm  26158  psercn  26162  pserdvlem2  26164  abelthlem3  26169  logtayl  26392  dvcxp1  26472  dvcncxp1  26475  logbmpt  26517  dmarea  26686  lgamgulmlem2  26758  lgamgulmlem5  26761  musum  26919  dchrptlem2  26992  dchrptlem3  26993  dchrpt  26994  lgsval  27028  lgsval4lem  27035  lgsneg  27048  lgsmod  27050  rpvmasum2  27239  padicfval  27343  ostth2  27364  ostth3  27365  ostth  27366  lmif  28291  islmib  28293  incistruhgr  28594  eucrct2eupth  29753  htthlem  30425  htth  30426  pjhfval  30904  hosmval  31243  hommval  31244  hodmval  31245  hfsmval  31246  hfmmval  31247  brafval  31451  kbfval  31460  mptprop  32175  psgnfzto1st  32522  linds2eq  32759  elrspunidl  32808  elrspunsn  32809  lbsdiflsp0  32987  fedgmullem1  32990  fedgmullem2  32991  fedgmul  32992  evls1fldgencl  33021  mdetpmtr1  33089  zar0ring  33144  ordtcnvNEW  33186  ordtrest2NEW  33189  xrhval  33284  indval  33297  esum2dlem  33376  ofceq  33381  itgeq12dv  33611  ballotlemfval  33774  vtsval  33935  lpadval  33974  ptpconn  34510  cvmliftlem15  34575  cvmlift2lem4  34583  cvmlift2  34593  snmlval  34608  snmlflim  34609  satf  34630  mrsubfval  34785  mrsubrn  34790  elmsubrn  34805  msubrn  34806  msubco  34808  faclim  35008  faclim2  35010  gg-dvfsumle  35468  gg-dvfsumlem2  35469  knoppcnlem1  35672  knoppcnlem6  35677  knoppcnlem7  35678  bj-evaleq  36256  csbrdgg  36513  curfv  36771  matunitlindflem2  36788  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem10  36801  poimirlem11  36802  poimirlem12  36803  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem18  36809  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem27  36818  voliunnfl  36835  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  itg2gt0cn  36846  iblabsnclem  36854  iblmulc2nc  36856  ftc1anclem2  36865  ftc1anclem6  36869  ftc1anclem8  36871  ftc1anc  36872  ftc2nc  36873  upixp  36900  rrncmslem  37003  ismrer1  37009  tendoplcbv  39949  tendopl  39950  tendoicbv  39967  tendoi  39968  dihfval  40405  lcfl7N  40675  lcfrlem8  40723  lcfrlem9  40724  lcf1o  40725  hvmapval  40934  hdmap1fval  40970  hdmapffval  41000  hdmapfval  41001  hgmapffval  41059  hgmapfval  41060  lcmineqlem7  41206  lcmineqlem12  41211  rhmmpl  41427  evlsvval  41434  evlsvvval  41437  evlsbagval  41440  selvvvval  41459  evlselv  41461  fsuppind  41464  fsuppssindlem2  41466  fsuppssind  41467  mzpclval  41765  mzpcl2  41770  mzpexpmpt  41785  mzpsubst  41788  mzpcompact2lem  41791  rmxfval  41944  rmyfval  41945  aomclem8  42105  hbtlem1  42167  hbtlem7  42169  rfovfvd  43055  fsovrfovd  43062  fsovfvd  43063  fsovcnvlem  43066  dssmapfv2d  43071  dssmapnvod  43073  ntrneibex  43126  mnringmulrvald  43288  mnringmulrcld  43289  expgrowthi  43394  expgrowth  43396  binomcxplemdvsum  43416  addrval  43527  subrval  43528  mulvval  43529  fmulcl  44596  fmuldfeqlem1  44597  fprodcnlem  44614  fprodcn  44615  fnlimfv  44678  fnlimcnv  44682  fnlimfvre  44689  fnlimfvre2  44692  fnlimf  44693  fnlimabslt  44694  liminfval  44774  limsupresxr  44781  liminfresxr  44782  liminfvalxr  44798  fprodcncf  44915  dvnmptdivc  44953  dvnxpaek  44957  dvnmul  44958  dvmptfprod  44960  dvnprodlem1  44961  dvnprodlem2  44962  dvnprodlem3  44963  dvnprod  44964  stoweidlem2  45017  stoweidlem17  45032  stoweidlem19  45034  stoweidlem20  45035  stoweidlem43  45058  stoweidlem62  45077  stoweid  45078  dirkercncflem2  45119  fourierdlem112  45233  fourierdlem113  45234  etransclem1  45250  etransclem5  45254  etransclem17  45266  etransclem19  45268  etransclem22  45271  sge0val  45381  ovnlecvr  45573  ovncvrrp  45579  ovn0lem  45580  ovnsubaddlem1  45585  ovnsubadd  45587  hsphoif  45591  hsphoival  45594  hoidmv1lelem1  45606  hoidmv1lelem2  45607  hoidmv1lelem3  45608  hoidmv1le  45609  hoidmvlelem1  45610  hoidmvlelem2  45611  hoidmvlelem3  45612  hoidmvlelem4  45613  hoidmvlelem5  45614  hoidmvle  45615  ovnhoilem1  45616  ovnhoi  45618  hoidifhspval  45623  ovncvr2  45626  hoidifhspval2  45630  hspmbllem2  45642  hspmbllem3  45643  hspmbl  45644  ovnovollem1  45671  vonioolem2  45696  vonioo  45697  vonicclem2  45699  vonicc  45700  smflimlem4  45789  smflim  45792  smflim2  45821  smfsuplem2  45827  smfsup  45829  smfinf  45833  smflimsuplem2  45836  smflimsuplem5  45839  smflimsuplem7  45841  smflimsup  45843  cfsetsnfsetfo  46069  lincop  47177  1arymaptfv  47414  itcoval  47435  itcovalpc  47446  itcovalt2  47451  ackvalsuc1mpt  47452  ackval1  47455  aacllem  47936