Theorem mpteq2dv 5192

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-mpt 5180

This theorem is referenced by:  ifmpt2v  7460  ofeqd  7624  mpocurryvald  8212  rdgeq1  8342  rdgeq2  8343  omv  8439  oev  8441  oieq1  9417  oieq2  9418  cantnflem1  9598  wunex2  10649  wuncval2  10658  rpnnen1  12896  seqof2  13983  relexpsucnnr  14948  relexp1g  14949  limsupval  15397  sumeq2w  15615  sumeq2ii  15616  cbvsum  15618  cbvsumv  15619  sumeq2sdv  15626  summo  15640  fsum  15643  fsumrlim  15734  fsumo1  15735  prodeq1  15830  prodeq2w  15833  prodeq2sdv  15846  prodmo  15859  fprod  15864  bpolylem  15971  rpnnen2lem1  16139  rpnnen2lem2  16140  1arithlem1  16851  vdwapval  16901  vdwlem6  16914  vdwlem8  16916  vdwlem9  16917  vdwlem10  16918  ramub1lem2  16955  ramcl  16957  sloteq  17110  prdsplusgval  17393  prdsmulrval  17395  prdsdsval  17398  prdsvscaval  17399  ismon  17657  fucco  17889  curf1  18148  curf2  18152  yonedalem4a  18198  smndex1gbas  18827  smndex1gid  18828  grplactfval  18971  galactghm  19333  pmtrval  19380  sylow1  19532  sylow2b  19552  sylow3lem5  19560  sylow3  19562  iscyg  19808  gsumzaddlem  19850  gsumzmhm  19866  ablfac2  20020  gsumdixp  20254  c0rhm  20467  c0rnghm  20468  zncyg  21503  phllmhm  21587  isphld  21609  frlmgsum  21727  frlmipval  21734  frlmphl  21736  uvcval  21740  fczpsrbag  21877  psrmulfval  21899  psrascl  21934  mvrval  21937  subrgmvr  21988  mplcoe1  21992  mplcoe3  21993  mplcoe5  21995  mplmon2  22016  subrgascl  22021  evlslem2  22034  evlslem3  22035  evlslem1  22037  mpfrcl  22040  evlsval  22041  evlsvval  22045  evlsvvval  22048  evlsvar  22050  mpfind  22070  selvfval  22077  selvval  22078  mhpfval  22081  psdfval  22101  psdval  22102  psdmvr  22112  coe1fval  22146  pf1ind  22299  evl1gsumadd  22302  rhmmpl  22327  rhmply1vr1  22331  mamuval  22337  mamufv  22338  matgsum  22381  madetsumid  22405  mat1dimmul  22420  mvmulval  22487  mvmulfv  22488  mavmulfv  22490  1mavmul  22492  marepvval0  22510  mulmarep1gsum1  22517  mdetleib  22531  mdetleib2  22532  mdetfval1  22534  mdetleib1  22535  mdet0pr  22536  m1detdiag  22541  mdetralt  22552  mdetunilem9  22564  m2detleib  22575  smadiadetlem3  22612  mat2pmatmul  22675  decpmatmul  22716  decpmatmulsumfsupp  22717  pmatcollpw1  22720  monmatcollpw  22723  pmatcollpw3lem  22727  pmatcollpw3fi1lem2  22731  pm2mpval  22739  pm2mpfval  22740  mply1topmatval  22748  mp2pm2mplem1  22750  mp2pm2mplem3  22752  ptbasfi  23525  ptcnplem  23565  ptrescn  23583  cnmpt2k  23632  xkohmeo  23759  fmval  23887  fmf  23889  ptcmpg  24001  tmdmulg  24036  prdstmdd  24068  tsmspropd  24076  prdsxmslem2  24473  metdsval  24792  fsumcn  24817  expcn  24819  expcnOLD  24821  lebnumlem3  24918  pcoval  24967  pi1xfrcnv  25013  cphsscph  25207  rrxds  25349  rrxmval  25361  itg11  25648  mbfi1fseqlem2  25673  mbfi1fseqlem6  25677  mbfi1fseq  25678  mbfi1flimlem  25679  mbfmullem  25682  itg2const  25697  itg2mulc  25704  itg2monolem1  25707  itg2i1fseqle  25711  itg2i1fseq  25712  itg2addlem  25715  itg2cnlem1  25718  itg2cn  25720  isibl  25722  isibl2  25723  iblitg  25725  itgeq1  25730  itgz  25738  itgvallem  25742  itgvallem3  25743  iblcnlem1  25745  itgcnlem  25747  iblrelem  25748  iblposlem  25749  iblpos  25750  itgrevallem1  25752  itgposval  25753  iblss2  25763  itgss  25769  itgfsum  25784  iblabslem  25785  iblmulc2  25788  bddmulibl  25796  itgcn  25802  ellimc  25830  dvnfval  25880  cpnfval  25890  dvexp  25913  dvexp2  25914  dvmptfsum  25935  dvlipcn  25955  dvivthlem1  25969  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  itgpowd  26013  elply2  26157  elplyr  26162  elplyd  26163  coeeu  26186  coelem  26187  coeeq  26188  plyco  26202  coe11  26214  coe1termlem  26219  dgrcolem1  26235  dvply2g  26248  dvply2gOLD  26249  elqaalem3  26285  eltayl  26323  tayl0  26325  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmcau  26360  ulmdvlem1  26365  ulmdvlem3  26367  mtest  26369  mtestbdd  26370  pserval  26375  pserulm  26387  psercn  26392  pserdvlem2  26394  abelthlem3  26399  logtayl  26625  dvcxp1  26705  dvcncxp1  26708  logbmpt  26754  dmarea  26923  lgamgulmlem2  26996  lgamgulmlem5  26999  musum  27157  dchrptlem2  27232  dchrptlem3  27233  dchrpt  27234  lgsval  27268  lgsval4lem  27275  lgsneg  27288  lgsmod  27290  rpvmasum2  27479  padicfval  27583  ostth2  27604  ostth3  27605  ostth  27606  lmif  28857  islmib  28859  incistruhgr  29152  eucrct2eupth  30320  htthlem  30992  htth  30993  pjhfval  31471  hosmval  31810  hommval  31811  hodmval  31812  hfsmval  31813  hfmmval  31814  brafval  32018  kbfval  32027  mptprop  32777  indval  32932  indsn  32945  psgnfzto1st  33187  fxpsubm  33254  fxpsubg  33255  fxpsubrg  33256  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspn  33328  elrgspnsubrunlem1  33329  linds2eq  33462  elrspunidl  33509  elrspunsn  33510  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  extvfval  33697  extvfv  33698  mvrvalind  33703  evlextv  33707  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  splysubrg  33718  issply  33719  esplyval  33720  vietalem  33735  vieta  33736  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunlsp  33831  extdgfialglem2  33850  mdetpmtr1  33980  zar0ring  34035  ordtcnvNEW  34077  ordtrest2NEW  34080  xrhval  34175  esum2dlem  34249  ofceq  34254  itgeq12dv  34483  ballotlemfval  34647  vtsval  34794  lpadval  34833  ptpconn  35427  cvmliftlem15  35492  cvmlift2lem4  35500  cvmlift2  35510  snmlval  35525  snmlflim  35526  satf  35547  mrsubfval  35702  mrsubrn  35707  elmsubrn  35722  msubrn  35723  msubco  35725  faclim  35940  faclim2  35942  prodeq12sdv  36412  itgeq12sdv  36413  cbvsumdavw  36473  cbvproddavw  36474  cbvsumdavw2  36489  cbvproddavw2  36490  knoppcnlem1  36693  knoppcnlem6  36698  knoppcnlem7  36699  bj-evaleq  37277  csbrdgg  37534  curfv  37801  matunitlindflem2  37818  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem27  37848  voliunnfl  37865  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  itg2gt0cn  37876  iblabsnclem  37884  iblmulc2nc  37886  ftc1anclem2  37895  ftc1anclem6  37899  ftc1anclem8  37901  ftc1anc  37902  ftc2nc  37903  upixp  37930  rrncmslem  38033  ismrer1  38039  tendoplcbv  41035  tendopl  41036  tendoicbv  41053  tendoi  41054  dihfval  41491  lcfl7N  41761  lcfrlem8  41809  lcfrlem9  41810  lcf1o  41811  hvmapval  42020  hdmap1fval  42056  hdmapffval  42086  hdmapfval  42087  hgmapffval  42145  hgmapfval  42146  lcmineqlem7  42289  lcmineqlem12  42294  aks6d1c6lem5  42431  rhmpsr  42805  evlsbagval  42812  selvvvval  42828  evlselv  42830  fsuppind  42833  fsuppssindlem2  42835  fsuppssind  42836  mzpclval  42967  mzpcl2  42972  mzpexpmpt  42987  mzpsubst  42990  mzpcompact2lem  42993  rmxfval  43146  rmyfval  43147  aomclem8  43303  hbtlem1  43365  hbtlem7  43367  rfovfvd  44243  fsovrfovd  44250  fsovfvd  44251  fsovcnvlem  44254  dssmapfv2d  44259  dssmapnvod  44261  ntrneibex  44314  mnringmulrvald  44468  mnringmulrcld  44469  expgrowthi  44574  expgrowth  44576  binomcxplemdvsum  44596  addrval  44706  subrval  44707  mulvval  44708  fmulcl  45827  fmuldfeqlem1  45828  fprodcnlem  45845  fprodcn  45846  fnlimfv  45907  fnlimcnv  45911  fnlimfvre  45918  fnlimfvre2  45921  fnlimf  45922  fnlimabslt  45923  liminfval  46003  limsupresxr  46010  liminfresxr  46011  liminfvalxr  46027  fprodcncf  46144  dvnmptdivc  46182  dvnxpaek  46186  dvnmul  46187  dvmptfprod  46189  dvnprodlem1  46190  dvnprodlem2  46191  dvnprodlem3  46192  dvnprod  46193  stoweidlem2  46246  stoweidlem17  46261  stoweidlem19  46263  stoweidlem20  46264  stoweidlem43  46287  stoweidlem62  46306  stoweid  46307  dirkercncflem2  46348  fourierdlem112  46462  fourierdlem113  46463  etransclem1  46479  etransclem5  46483  etransclem17  46495  etransclem19  46497  etransclem22  46500  sge0val  46610  ovnlecvr  46802  ovncvrrp  46808  ovn0lem  46809  ovnsubaddlem1  46814  ovnsubadd  46816  hsphoif  46820  hsphoival  46823  hoidmv1lelem1  46835  hoidmv1lelem2  46836  hoidmv1lelem3  46837  hoidmv1le  46838  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  hoidmvlelem5  46843  hoidmvle  46844  ovnhoilem1  46845  ovnhoi  46847  hoidifhspval  46852  ovncvr2  46855  hoidifhspval2  46859  hspmbllem2  46871  hspmbllem3  46872  hspmbl  46873  ovnovollem1  46900  vonioolem2  46925  vonioo  46926  vonicclem2  46928  vonicc  46929  smflimlem4  47018  smflim  47021  smflim2  47050  smfsuplem2  47056  smfsup  47058  smfinf  47062  smflimsuplem2  47065  smflimsuplem5  47068  smflimsuplem7  47070  smflimsup  47072  cfsetsnfsetfo  47306  lincop  48654  1arymaptfv  48886  itcoval  48907  itcovalpc  48918  itcovalt2  48923  ackvalsuc1mpt  48924  ackval1  48927  fuco21  49581  prcofval  49623  aacllem  50046