Theorem mpteq2dv 5179

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5166

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-mpt 5167

This theorem is referenced by:  ifmpt2v  7469  ofeqd  7633  mpocurryvald  8220  rdgeq1  8350  rdgeq2  8351  omv  8447  oev  8449  oieq1  9427  oieq2  9428  cantnflem1  9610  wunex2  10661  wuncval2  10670  indval  12162  rpnnen1  12933  seqof2  14022  relexpsucnnr  14987  relexp1g  14988  limsupval  15436  sumeq2w  15654  sumeq2ii  15655  cbvsum  15657  cbvsumv  15658  sumeq2sdv  15665  summo  15679  fsum  15682  fsumrlim  15774  fsumo1  15775  prodeq1  15872  prodeq2w  15875  prodeq2sdv  15888  prodmo  15901  fprod  15906  bpolylem  16013  rpnnen2lem1  16181  rpnnen2lem2  16182  1arithlem1  16894  vdwapval  16944  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwlem10  16961  ramub1lem2  16998  ramcl  17000  sloteq  17153  prdsplusgval  17436  prdsmulrval  17438  prdsdsval  17441  prdsvscaval  17442  ismon  17700  fucco  17932  curf1  18191  curf2  18195  yonedalem4a  18241  smndex1gbas  18870  smndex1gbasOLD  18871  smndex1gid  18872  smndex1gidOLD  18873  smndex1igid  18874  grplactfval  19017  galactghm  19379  pmtrval  19426  sylow1  19578  sylow2b  19598  sylow3lem5  19606  sylow3  19608  iscyg  19854  gsumzaddlem  19896  gsumzmhm  19912  ablfac2  20066  gsumdixp  20298  c0rhm  20511  c0rnghm  20512  zncyg  21528  phllmhm  21612  isphld  21634  frlmgsum  21752  frlmipval  21759  frlmphl  21761  uvcval  21765  fczpsrbag  21901  psrmulfval  21922  psrascl  21957  mvrval  21960  subrgmvr  22011  mplcoe1  22015  mplcoe3  22016  mplcoe5  22018  mplmon2  22039  subrgascl  22044  evlslem2  22057  evlslem3  22058  evlslem1  22060  mpfrcl  22063  evlsval  22064  evlsvval  22068  evlsvvval  22071  evlsvar  22073  mpfind  22093  selvfval  22100  selvval  22101  mhpfval  22104  psdfval  22124  psdval  22125  psdmvr  22135  coe1fval  22169  pf1ind  22320  evl1gsumadd  22323  rhmmpl  22348  rhmply1vr1  22352  mamuval  22358  mamufv  22359  matgsum  22402  madetsumid  22426  mat1dimmul  22441  mvmulval  22508  mvmulfv  22509  mavmulfv  22511  1mavmul  22513  marepvval0  22531  mulmarep1gsum1  22538  mdetleib  22552  mdetleib2  22553  mdetfval1  22555  mdetleib1  22556  mdet0pr  22557  m1detdiag  22562  mdetralt  22573  mdetunilem9  22585  m2detleib  22596  smadiadetlem3  22633  mat2pmatmul  22696  decpmatmul  22737  decpmatmulsumfsupp  22738  pmatcollpw1  22741  monmatcollpw  22744  pmatcollpw3lem  22748  pmatcollpw3fi1lem2  22752  pm2mpval  22760  pm2mpfval  22761  mply1topmatval  22769  mp2pm2mplem1  22771  mp2pm2mplem3  22773  ptbasfi  23546  ptcnplem  23586  ptrescn  23604  cnmpt2k  23653  xkohmeo  23780  fmval  23908  fmf  23910  ptcmpg  24022  tmdmulg  24057  prdstmdd  24089  tsmspropd  24097  prdsxmslem2  24494  metdsval  24813  fsumcn  24837  expcn  24839  lebnumlem3  24930  pcoval  24978  pi1xfrcnv  25024  cphsscph  25218  rrxds  25360  rrxmval  25372  itg11  25658  mbfi1fseqlem2  25683  mbfi1fseqlem6  25687  mbfi1fseq  25688  mbfi1flimlem  25689  mbfmullem  25692  itg2const  25707  itg2mulc  25714  itg2monolem1  25717  itg2i1fseqle  25721  itg2i1fseq  25722  itg2addlem  25725  itg2cnlem1  25728  itg2cn  25730  isibl  25732  isibl2  25733  iblitg  25735  itgeq1  25740  itgz  25748  itgvallem  25752  itgvallem3  25753  iblcnlem1  25755  itgcnlem  25757  iblrelem  25758  iblposlem  25759  iblpos  25760  itgrevallem1  25762  itgposval  25763  iblss2  25773  itgss  25779  itgfsum  25794  iblabslem  25795  iblmulc2  25798  bddmulibl  25806  itgcn  25812  ellimc  25840  dvnfval  25889  cpnfval  25899  dvexp  25920  dvexp2  25921  dvmptfsum  25942  dvlipcn  25961  dvivthlem1  25975  dvfsumle  25988  dvfsumabs  25990  dvfsumlem2  25994  itgpowd  26017  elply2  26161  elplyr  26166  elplyd  26167  coeeu  26190  coelem  26191  coeeq  26192  plyco  26206  coe11  26218  coe1termlem  26223  dgrcolem1  26238  dvply2g  26251  elqaalem3  26287  eltayl  26325  tayl0  26327  taylthlem1  26338  taylthlem2  26339  ulmcau  26360  ulmdvlem1  26365  ulmdvlem3  26367  mtest  26369  mtestbdd  26370  pserval  26375  pserulm  26387  psercn  26391  pserdvlem2  26393  abelthlem3  26398  logtayl  26624  dvcxp1  26704  dvcncxp1  26707  logbmpt  26752  dmarea  26921  lgamgulmlem2  26993  lgamgulmlem5  26996  musum  27154  dchrptlem2  27228  dchrptlem3  27229  dchrpt  27230  lgsval  27264  lgsval4lem  27271  lgsneg  27284  lgsmod  27286  rpvmasum2  27475  padicfval  27579  ostth2  27600  ostth3  27601  ostth  27602  lmif  28853  islmib  28855  incistruhgr  29148  eucrct2eupth  30315  htthlem  30988  htth  30989  pjhfval  31467  hosmval  31806  hommval  31807  hodmval  31808  hfsmval  31809  hfmmval  31810  brafval  32014  kbfval  32023  mptprop  32771  indsn  32923  psgnfzto1st  33166  fxpsubm  33233  fxpsubg  33234  fxpsubrg  33235  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspn  33307  elrgspnsubrunlem1  33308  linds2eq  33441  elrspunidl  33488  elrspunsn  33489  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  extvfval  33676  extvfv  33677  mvrvalind  33682  evlextv  33686  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrgsum  33692  psrmonmul2  33695  psrmonprod  33696  splysubrg  33704  issply  33705  esplyval  33706  esplyfvaln  33718  vietalem  33723  vieta  33724  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspunlsp  33818  extdgfialglem2  33837  mdetpmtr1  33967  zar0ring  34022  ordtcnvNEW  34064  ordtrest2NEW  34067  xrhval  34162  esum2dlem  34236  ofceq  34241  itgeq12dv  34470  ballotlemfval  34634  vtsval  34781  lpadval  34820  ptpconn  35415  cvmliftlem15  35480  cvmlift2lem4  35488  cvmlift2  35498  snmlval  35513  snmlflim  35514  satf  35535  mrsubfval  35690  mrsubrn  35695  elmsubrn  35710  msubrn  35711  msubco  35713  faclim  35928  faclim2  35930  prodeq12sdv  36400  itgeq12sdv  36401  cbvsumdavw  36461  cbvproddavw  36462  cbvsumdavw2  36477  cbvproddavw2  36478  knoppcnlem1  36753  knoppcnlem6  36758  knoppcnlem7  36759  bj-evaleq  37383  csbrdgg  37645  curfv  37921  matunitlindflem2  37938  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem27  37968  voliunnfl  37985  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  iblabsnclem  38004  iblmulc2nc  38006  ftc1anclem2  38015  ftc1anclem6  38019  ftc1anclem8  38021  ftc1anc  38022  ftc2nc  38023  upixp  38050  rrncmslem  38153  ismrer1  38159  tendoplcbv  41221  tendopl  41222  tendoicbv  41239  tendoi  41240  dihfval  41677  lcfl7N  41947  lcfrlem8  41995  lcfrlem9  41996  lcf1o  41997  hvmapval  42206  hdmap1fval  42242  hdmapffval  42272  hdmapfval  42273  hgmapffval  42331  hgmapfval  42332  lcmineqlem7  42474  lcmineqlem12  42479  aks6d1c6lem5  42616  rhmpsr  42995  evlsbagval  43002  selvvvval  43018  evlselv  43020  fsuppind  43023  fsuppssindlem2  43025  fsuppssind  43026  mzpclval  43157  mzpcl2  43162  mzpexpmpt  43177  mzpsubst  43180  mzpcompact2lem  43183  rmxfval  43332  rmyfval  43333  aomclem8  43489  hbtlem1  43551  hbtlem7  43553  rfovfvd  44429  fsovrfovd  44436  fsovfvd  44437  fsovcnvlem  44440  dssmapfv2d  44445  dssmapnvod  44447  ntrneibex  44500  mnringmulrvald  44654  mnringmulrcld  44655  expgrowthi  44760  expgrowth  44762  binomcxplemdvsum  44782  addrval  44892  subrval  44893  mulvval  44894  fmulcl  46011  fmuldfeqlem1  46012  fprodcnlem  46029  fprodcn  46030  fnlimfv  46091  fnlimcnv  46095  fnlimfvre  46102  fnlimfvre2  46105  fnlimf  46106  fnlimabslt  46107  liminfval  46187  limsupresxr  46194  liminfresxr  46195  liminfvalxr  46211  fprodcncf  46328  dvnmptdivc  46366  dvnxpaek  46370  dvnmul  46371  dvmptfprod  46373  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  dvnprod  46377  stoweidlem2  46430  stoweidlem17  46445  stoweidlem19  46447  stoweidlem20  46448  stoweidlem43  46471  stoweidlem62  46490  stoweid  46491  dirkercncflem2  46532  fourierdlem112  46646  fourierdlem113  46647  etransclem1  46663  etransclem5  46667  etransclem17  46679  etransclem19  46681  etransclem22  46684  sge0val  46794  ovnlecvr  46986  ovncvrrp  46992  ovn0lem  46993  ovnsubaddlem1  46998  ovnsubadd  47000  hsphoif  47004  hsphoival  47007  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hoidmvle  47028  ovnhoilem1  47029  ovnhoi  47031  hoidifhspval  47036  ovncvr2  47039  hoidifhspval2  47043  hspmbllem2  47055  hspmbllem3  47056  hspmbl  47057  ovnovollem1  47084  vonioolem2  47109  vonioo  47110  vonicclem2  47112  vonicc  47113  smflimlem4  47202  smflim  47205  smflim2  47234  smfsuplem2  47240  smfsup  47242  smfinf  47246  smflimsuplem2  47249  smflimsuplem5  47252  smflimsuplem7  47254  smflimsup  47256  cfsetsnfsetfo  47508  lincop  48884  1arymaptfv  49116  itcoval  49137  itcovalpc  49148  itcovalt2  49153  ackvalsuc1mpt  49154  ackval1  49157  fuco21  49811  prcofval  49853  aacllem  50276