Theorem mpteq2dv 5199

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-mpt 5187

This theorem is used by:  ifmpt2v  7520  ofeqd  7693  mpocurryvald  8280  rdgeq1  8412  rdgeq2  8413  omv  8513  oev  8515  curfv  8885  oieq1  9499  oieq2  9500  cantnflem1  9683  wunex2  10816  wuncval2  10825  indval  12316  rpnnen1  13104  seqof2  14196  relexpsucnnr  15171  relexp1g  15172  limsupval  15634  sumeq2w  15852  sumeq2ii  15853  cbvsum  15855  cbvsumv  15856  sumeq2sdv  15863  summo  15876  fsum  15879  fsumrlim  15971  fsumo1  15972  prodeq1  16069  prodeq2w  16072  prodeq2sdv  16084  prodmo  16096  fprod  16101  bpolylem  16207  rpnnen2lem1  16375  rpnnen2lem2  16376  1arithlem1  17094  vdwapval  17144  vdwlem6  17157  vdwlem8  17159  vdwlem9  17160  vdwlem10  17161  ramub1lem2  17198  ramcl  17200  sloteq  17354  prdsplusgval  17637  prdsmulrval  17639  prdsdsval  17642  prdsvscaval  17643  ismon  17901  fucco  18133  curf1  18392  curf2  18396  yonedalem4a  18442  smndex1gbas  19091  smndex1gbasOLD  19092  smndex1gid  19093  smndex1gidOLD  19094  smndex1igid  19095  grplactfval  19244  galactghm  19611  pmtrval  19658  sylow1  19810  sylow2b  19830  sylow3lem5  19838  sylow3  19840  iscyg  20086  gsumzaddlem  20128  gsumzmhm  20144  ablfac2  20298  gsumdixp  20541  c0rhm  20779  c0rnghm  20780  zncyg  21847  phllmhm  21931  isphld  21953  frlmgsum  22071  frlmipval  22078  frlmphl  22080  uvcval  22084  fczpsrbag  22222  psrmulfval  22244  psrascl  22279  mvrval  22282  subrgmvr  22335  mplcoe1  22339  mplcoe3  22340  mplcoe5  22342  mplmon2  22363  subrgascl  22368  evlslem2  22381  evlslem3  22382  evlslem1  22384  mpfrcl  22387  evlsval  22388  evlsvval  22392  evlsvvval  22395  evlsvar  22397  mpfind  22417  selvfval  22421  selvval  22422  selvvvval  22444  mhpfval  22452  psdfval  22472  psdval  22473  psdmvr  22483  coe1fval  22516  pf1ind  22666  evl1gsumadd  22669  rhmmpl  22691  rhmply1vr1  22695  mamuval  22701  mamufv  22702  matgsum  22745  madetsumid  22769  mat1dimmul  22784  mvmulval  22851  mvmulfv  22852  mavmulfv  22854  1mavmul  22856  marepvval0  22874  mulmarep1gsum1  22881  mdetleib  22895  mdetleib2  22896  mdetfval1  22898  mdetleib1  22899  mdet0pr  22900  m1detdiag  22905  mdetralt  22916  mdetunilem9  22928  m2detleib  22939  smadiadetlem3  22976  matunitlindflem2  22988  mat2pmatmul  23042  decpmatmul  23083  decpmatmulsumfsupp  23084  pmatcollpw1  23087  monmatcollpw  23090  pmatcollpw3lem  23094  pmatcollpw3fi1lem2  23098  pm2mpval  23106  pm2mpfval  23107  mply1topmatval  23115  mp2pm2mplem1  23117  mp2pm2mplem3  23119  ptbasfi  23893  ptcnplem  23933  ptrescn  23951  cnmpt2k  24000  xkohmeo  24127  fmval  24255  fmf  24257  ptcmpg  24369  tmdmulg  24404  prdstmdd  24436  tsmspropd  24444  prdsxmslem2  24841  metdsval  25160  fsumcn  25184  expcn  25186  lebnumlem3  25277  pcoval  25325  pi1xfrcnv  25371  cphsscph  25565  rrxds  25707  rrxmval  25719  itg11  26005  mbfi1fseqlem2  26030  mbfi1fseqlem6  26034  mbfi1fseq  26035  mbfi1flimlem  26036  mbfmullem  26039  itg2const  26054  itg2mulc  26061  itg2monolem1  26064  itg2i1fseqle  26068  itg2i1fseq  26069  itg2addlem  26072  itg2cnlem1  26075  itg2cn  26077  isibl  26079  isibl2  26080  iblitg  26082  itgeq1  26086  itgz  26094  itgvallem  26098  itgvallem3  26099  iblcnlem1  26101  itgcnlem  26103  iblrelem  26104  iblposlem  26105  iblpos  26106  itgrevallem1  26108  itgposval  26109  iblss2  26119  itgss  26125  itgfsum  26140  iblabslem  26141  iblmulc2  26144  bddmulibl  26152  itgcn  26158  ellimc  26186  dvnfval  26235  cpnfval  26245  dvexp  26266  dvexp2  26267  dvmptfsum  26288  dvlipcn  26307  dvivthlem1  26321  dvfsumle  26334  dvfsumabs  26336  dvfsumlem2  26340  itgpowd  26363  elply2  26507  elplyr  26512  elplyd  26513  coeeu  26537  coelem  26538  coeeq  26539  plyco  26553  coe11  26565  coe1termlem  26570  dgrcolem1  26585  dvply2g  26599  elqaalem3  26637  eltayl  26680  tayl0  26682  taylthlem1  26693  taylthlem2  26694  ulmcau  26715  ulmdvlem1  26720  ulmdvlem3  26722  mtest  26724  mtestbdd  26725  pserval  26730  pserulm  26742  psercn  26746  pserdvlem2  26748  abelthlem3  26753  logtayl  26981  dvcxp1  27061  dvcncxp1  27064  logbmpt  27109  dmarea  27278  lgamgulmlem2  27350  lgamgulmlem5  27353  musum  27511  dchrptlem2  27585  dchrptlem3  27586  dchrpt  27587  lgsval  27621  lgsval4lem  27628  lgsneg  27641  lgsmod  27643  rpvmasum2  27832  padicfval  27936  ostth2  27957  ostth3  27958  ostth  27959  lmif  29283  islmib  29285  incistruhgr  29650  eucrct2eupth  30839  htthlem  31512  htth  31513  pjhfval  31991  hosmval  32330  hommval  32331  hodmval  32332  hfsmval  32333  hfmmval  32334  brafval  32538  kbfval  32547  mptprop  33284  indsn  33423  psgnfzto1st  33659  fxpsubm  33726  fxpsubg  33727  fxpsubrg  33728  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnlem3  33798  elrgspnlem4  33799  elrgspn  33800  elrgspnsubrunlem1  33801  linds2eq  33929  elrspunidl  33971  elrspunsn  33972  evl1deg1  34101  evl1deg2  34102  evl1deg3  34103  mplasclco  34141  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem2  34146  selvply1rhmlem3  34147  selvply1rhmlem4  34148  selvply1rhmlem5  34149  selvply1rhm  34150  mplidom  34153  extvfval  34157  extvfv  34158  mvrvalind  34163  evlextv  34167  mplvrpmfgalem  34169  mplvrpmga  34170  mplvrpmmhm  34171  mplvrpmrhm  34172  psrgsum  34173  psrmonmul2  34176  psrmonprod  34177  splysubrg  34185  issply  34186  esplyval  34187  esplyfvaln  34199  vietalem  34204  vieta  34205  lbsdiflsp0  34251  fedgmullem1  34254  fedgmullem2  34255  fedgmul  34256  evls1fldgencl  34295  fldextrspunlsplem  34298  fldextrspunlsp  34299  extdgfialglem2  34318  mdetpmtr1  34448  zar0ring  34503  ordtcnvNEW  34545  ordtrest2NEW  34548  xrhval  34643  esum2dlem  34717  ofceq  34722  itgeq12dv  34951  ballotlemfval  35115  vtsval  35259  lpadval  35301  ptpconn  35977  cvmliftlem15  36042  cvmlift2lem4  36050  cvmlift2  36060  snmlval  36075  snmlflim  36076  satf  36097  mrsubfval  36252  mrsubrn  36257  elmsubrn  36272  msubrn  36273  msubco  36275  faclim  36490  faclim2  36492  prodeq12sdv  36987  itgeq12sdv  36988  cbvsumdavw  37048  cbvproddavw  37049  cbvsumdavw2  37064  cbvproddavw2  37065  knoppcnlem1  37339  knoppcnlem6  37344  knoppcnlem7  37345  bj-evaleq  37972  csbrdgg  38232  poimirlem5  38523  poimirlem6  38524  poimirlem7  38525  poimirlem8  38526  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem18  38536  poimirlem19  38537  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  poimirlem27  38545  voliunnfl  38562  itg2addnclem  38569  itg2addnclem3  38571  itg2addnc  38572  itg2gt0cn  38573  iblabsnclem  38581  iblmulc2nc  38583  ftc1anclem2  38592  ftc1anclem6  38596  ftc1anclem8  38598  ftc1anc  38599  ftc2nc  38600  upixp  38643  rrncmslem  38746  ismrer1  38752  tendoplcbv  41812  tendopl  41813  tendoicbv  41830  tendoi  41831  dihfval  42268  lcfl7N  42538  lcfrlem8  42586  lcfrlem9  42587  lcf1o  42588  hvmapval  42797  hdmap1fval  42833  hdmapffval  42863  hdmapfval  42864  hgmapffval  42922  hgmapfval  42923  lcmineqlem7  43065  lcmineqlem12  43070  aks6d1c6lem5  43207  rhmpsr  43591  evlsbagval  43594  evlselv  43597  fsuppind  43598  fsuppssindlem2  43600  fsuppssind  43601  mzpclval  43715  mzpcl2  43720  mzpexpmpt  43735  mzpsubst  43738  mzpcompact2lem  43741  rmxfval  43890  rmyfval  43891  aomclem8  44047  hbtlem1  44109  hbtlem7  44111  rfovfvd  44987  fsovrfovd  44994  fsovfvd  44995  fsovcnvlem  44998  dssmapfv2d  45003  dssmapnvod  45005  ntrneibex  45058  mnringmulrvald  45210  mnringmulrcld  45211  expgrowthi  45302  expgrowth  45304  binomcxplemdvsum  45324  addrval  45433  subrval  45434  mulvval  45435  fmulcl  46562  fmuldfeqlem1  46563  fprodcnlem  46580  fprodcn  46581  fnlimfv  46642  fnlimcnv  46646  fnlimfvre  46653  fnlimfvre2  46656  fnlimf  46657  fnlimabslt  46658  liminfval  46738  limsupresxr  46745  liminfresxr  46746  liminfvalxr  46762  fprodcncf  46879  dvnmptdivc  46917  dvnxpaek  46921  dvnmul  46922  dvmptfprod  46924  dvnprodlem1  46925  dvnprodlem2  46926  dvnprodlem3  46927  dvnprod  46928  stoweidlem2  46981  stoweidlem17  46996  stoweidlem19  46998  stoweidlem20  46999  stoweidlem43  47022  stoweidlem62  47041  stoweid  47042  dirkercncflem2  47083  fourierdlem112  47197  fourierdlem113  47198  etransclem1  47214  etransclem5  47218  etransclem17  47230  etransclem19  47232  etransclem22  47235  sge0val  47345  ovnlecvr  47537  ovncvrrp  47543  ovn0lem  47544  ovnsubaddlem1  47549  ovnsubadd  47551  hsphoif  47555  hsphoival  47558  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmv1lelem3  47572  hoidmv1le  47573  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem3  47576  hoidmvlelem4  47577  hoidmvlelem5  47578  hoidmvle  47579  ovnhoilem1  47580  ovnhoi  47582  hoidifhspval  47587  ovncvr2  47590  hoidifhspval2  47594  hspmbllem2  47606  hspmbllem3  47607  hspmbl  47608  ovnovollem1  47635  vonioolem2  47660  vonioo  47661  vonicclem2  47663  vonicc  47664  smflimlem4  47753  smflim  47756  smflim2  47785  smfsuplem2  47791  smfsup  47793  smfinf  47797  smflimsuplem2  47800  smflimsuplem5  47803  smflimsuplem7  47805  smflimsup  47807  cfsetsnfsetfo  48099  lincop  49489  1arymaptfv  49721  itcoval  49742  itcovalpc  49753  itcovalt2  49758  ackvalsuc1mpt  49759  ackval1  49762  fuco21  50413  prcofval  50455  aacllem  50908  crosspval  50923  crosspdot0lem  50932  veronesevald  50940  veronesematrowexpd  50951