Theorem mpteq2dv 5204

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-mpt 5192

This theorem is referenced by:  ifmpt2v  7494  ofeqd  7658  mpocurryvald  8252  rdgeq1  8382  rdgeq2  8383  omv  8479  oev  8481  oieq1  9472  oieq2  9473  cantnflem1  9649  wunex2  10698  wuncval2  10707  rpnnen1  12949  seqof2  14032  relexpsucnnr  14998  relexp1g  14999  limsupval  15447  sumeq2w  15665  sumeq2ii  15666  cbvsum  15668  cbvsumv  15669  sumeq2sdv  15676  summo  15690  fsum  15693  fsumrlim  15784  fsumo1  15785  prodeq1  15880  prodeq2w  15883  prodeq2sdv  15896  prodmo  15909  fprod  15914  bpolylem  16021  rpnnen2lem1  16189  rpnnen2lem2  16190  1arithlem1  16901  vdwapval  16951  vdwlem6  16964  vdwlem8  16966  vdwlem9  16967  vdwlem10  16968  ramub1lem2  17005  ramcl  17007  sloteq  17160  prdsplusgval  17443  prdsmulrval  17445  prdsdsval  17448  prdsvscaval  17449  ismon  17702  fucco  17934  curf1  18193  curf2  18197  yonedalem4a  18243  smndex1gbas  18836  smndex1gid  18837  grplactfval  18980  galactghm  19341  pmtrval  19388  sylow1  19540  sylow2b  19560  sylow3lem5  19568  sylow3  19570  iscyg  19816  gsumzaddlem  19858  gsumzmhm  19874  ablfac2  20028  gsumdixp  20235  c0rhm  20450  c0rnghm  20451  zncyg  21465  phllmhm  21548  isphld  21570  frlmgsum  21688  frlmipval  21695  frlmphl  21697  uvcval  21701  fczpsrbag  21837  psrmulfval  21859  psrascl  21895  mvrval  21898  subrgmvr  21947  mplcoe1  21951  mplcoe3  21952  mplcoe5  21954  mplmon2  21975  subrgascl  21980  evlslem2  21993  evlslem3  21994  evlslem1  21996  mpfrcl  21999  evlsval  22000  evlsvar  22004  mpfind  22021  selvfval  22028  selvval  22029  mhpfval  22032  psdfval  22052  psdval  22053  psdmvr  22063  coe1fval  22097  pf1ind  22249  evl1gsumadd  22252  rhmmpl  22277  rhmply1vr1  22281  mamuval  22287  mamufv  22288  matgsum  22331  madetsumid  22355  mat1dimmul  22370  mvmulval  22437  mvmulfv  22438  mavmulfv  22440  1mavmul  22442  marepvval0  22460  mulmarep1gsum1  22467  mdetleib  22481  mdetleib2  22482  mdetfval1  22484  mdetleib1  22485  mdet0pr  22486  m1detdiag  22491  mdetralt  22502  mdetunilem9  22514  m2detleib  22525  smadiadetlem3  22562  mat2pmatmul  22625  decpmatmul  22666  decpmatmulsumfsupp  22667  pmatcollpw1  22670  monmatcollpw  22673  pmatcollpw3lem  22677  pmatcollpw3fi1lem2  22681  pm2mpval  22689  pm2mpfval  22690  mply1topmatval  22698  mp2pm2mplem1  22700  mp2pm2mplem3  22702  ptbasfi  23475  ptcnplem  23515  ptrescn  23533  cnmpt2k  23582  xkohmeo  23709  fmval  23837  fmf  23839  ptcmpg  23951  tmdmulg  23986  prdstmdd  24018  tsmspropd  24026  prdsxmslem2  24424  metdsval  24743  fsumcn  24768  expcn  24770  expcnOLD  24772  lebnumlem3  24869  pcoval  24918  pi1xfrcnv  24964  cphsscph  25158  rrxds  25300  rrxmval  25312  itg11  25599  mbfi1fseqlem2  25624  mbfi1fseqlem6  25628  mbfi1fseq  25629  mbfi1flimlem  25630  mbfmullem  25633  itg2const  25648  itg2mulc  25655  itg2monolem1  25658  itg2i1fseqle  25662  itg2i1fseq  25663  itg2addlem  25666  itg2cnlem1  25669  itg2cn  25671  isibl  25673  isibl2  25674  iblitg  25676  itgeq1  25681  itgz  25689  itgvallem  25693  itgvallem3  25694  iblcnlem1  25696  itgcnlem  25698  iblrelem  25699  iblposlem  25700  iblpos  25701  itgrevallem1  25703  itgposval  25704  iblss2  25714  itgss  25720  itgfsum  25735  iblabslem  25736  iblmulc2  25739  bddmulibl  25747  itgcn  25753  ellimc  25781  dvnfval  25831  cpnfval  25841  dvexp  25864  dvexp2  25865  dvmptfsum  25886  dvlipcn  25906  dvivthlem1  25920  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgpowd  25964  elply2  26108  elplyr  26113  elplyd  26114  coeeu  26137  coelem  26138  coeeq  26139  plyco  26153  coe11  26165  coe1termlem  26170  dgrcolem1  26186  dvply2g  26199  dvply2gOLD  26200  elqaalem3  26236  eltayl  26274  tayl0  26276  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmcau  26311  ulmdvlem1  26316  ulmdvlem3  26318  mtest  26320  mtestbdd  26321  pserval  26326  pserulm  26338  psercn  26343  pserdvlem2  26345  abelthlem3  26350  logtayl  26576  dvcxp1  26656  dvcncxp1  26659  logbmpt  26705  dmarea  26874  lgamgulmlem2  26947  lgamgulmlem5  26950  musum  27108  dchrptlem2  27183  dchrptlem3  27184  dchrpt  27185  lgsval  27219  lgsval4lem  27226  lgsneg  27239  lgsmod  27241  rpvmasum2  27430  padicfval  27534  ostth2  27555  ostth3  27556  ostth  27557  lmif  28719  islmib  28721  incistruhgr  29013  eucrct2eupth  30181  htthlem  30853  htth  30854  pjhfval  31332  hosmval  31671  hommval  31672  hodmval  31673  hfsmval  31674  hfmmval  31675  brafval  31879  kbfval  31888  mptprop  32628  indval  32783  psgnfzto1st  33069  fxpsubm  33136  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspn  33204  elrgspnsubrunlem1  33205  linds2eq  33359  elrspunidl  33406  elrspunsn  33407  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspunlsp  33676  mdetpmtr1  33820  zar0ring  33875  ordtcnvNEW  33917  ordtrest2NEW  33920  xrhval  34015  esum2dlem  34089  ofceq  34094  itgeq12dv  34324  ballotlemfval  34488  vtsval  34635  lpadval  34674  ptpconn  35227  cvmliftlem15  35292  cvmlift2lem4  35300  cvmlift2  35310  snmlval  35325  snmlflim  35326  satf  35347  mrsubfval  35502  mrsubrn  35507  elmsubrn  35522  msubrn  35523  msubco  35525  faclim  35740  faclim2  35742  prodeq12sdv  36213  itgeq12sdv  36214  cbvsumdavw  36274  cbvproddavw  36275  cbvsumdavw2  36290  cbvproddavw2  36291  knoppcnlem1  36488  knoppcnlem6  36493  knoppcnlem7  36494  bj-evaleq  37067  csbrdgg  37324  curfv  37601  matunitlindflem2  37618  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem27  37648  voliunnfl  37665  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  iblabsnclem  37684  iblmulc2nc  37686  ftc1anclem2  37695  ftc1anclem6  37699  ftc1anclem8  37701  ftc1anc  37702  ftc2nc  37703  upixp  37730  rrncmslem  37833  ismrer1  37839  tendoplcbv  40776  tendopl  40777  tendoicbv  40794  tendoi  40795  dihfval  41232  lcfl7N  41502  lcfrlem8  41550  lcfrlem9  41551  lcf1o  41552  hvmapval  41761  hdmap1fval  41797  hdmapffval  41827  hdmapfval  41828  hgmapffval  41886  hgmapfval  41887  lcmineqlem7  42030  lcmineqlem12  42035  aks6d1c6lem5  42172  rhmpsr  42547  evlsvval  42555  evlsvvval  42558  evlsbagval  42561  selvvvval  42580  evlselv  42582  fsuppind  42585  fsuppssindlem2  42587  fsuppssind  42588  mzpclval  42720  mzpcl2  42725  mzpexpmpt  42740  mzpsubst  42743  mzpcompact2lem  42746  rmxfval  42899  rmyfval  42900  aomclem8  43057  hbtlem1  43119  hbtlem7  43121  rfovfvd  43998  fsovrfovd  44005  fsovfvd  44006  fsovcnvlem  44009  dssmapfv2d  44014  dssmapnvod  44016  ntrneibex  44069  mnringmulrvald  44223  mnringmulrcld  44224  expgrowthi  44329  expgrowth  44331  binomcxplemdvsum  44351  addrval  44462  subrval  44463  mulvval  44464  fmulcl  45586  fmuldfeqlem1  45587  fprodcnlem  45604  fprodcn  45605  fnlimfv  45668  fnlimcnv  45672  fnlimfvre  45679  fnlimfvre2  45682  fnlimf  45683  fnlimabslt  45684  liminfval  45764  limsupresxr  45771  liminfresxr  45772  liminfvalxr  45788  fprodcncf  45905  dvnmptdivc  45943  dvnxpaek  45947  dvnmul  45948  dvmptfprod  45950  dvnprodlem1  45951  dvnprodlem2  45952  dvnprodlem3  45953  dvnprod  45954  stoweidlem2  46007  stoweidlem17  46022  stoweidlem19  46024  stoweidlem20  46025  stoweidlem43  46048  stoweidlem62  46067  stoweid  46068  dirkercncflem2  46109  fourierdlem112  46223  fourierdlem113  46224  etransclem1  46240  etransclem5  46244  etransclem17  46256  etransclem19  46258  etransclem22  46261  sge0val  46371  ovnlecvr  46563  ovncvrrp  46569  ovn0lem  46570  ovnsubaddlem1  46575  ovnsubadd  46577  hsphoif  46581  hsphoival  46584  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hoidmvlelem5  46604  hoidmvle  46605  ovnhoilem1  46606  ovnhoi  46608  hoidifhspval  46613  ovncvr2  46616  hoidifhspval2  46620  hspmbllem2  46632  hspmbllem3  46633  hspmbl  46634  ovnovollem1  46661  vonioolem2  46686  vonioo  46687  vonicclem2  46689  vonicc  46690  smflimlem4  46779  smflim  46782  smflim2  46811  smfsuplem2  46817  smfsup  46819  smfinf  46823  smflimsuplem2  46826  smflimsuplem5  46829  smflimsuplem7  46831  smflimsup  46833  cfsetsnfsetfo  47065  lincop  48401  1arymaptfv  48633  itcoval  48654  itcovalpc  48665  itcovalt2  48670  ackvalsuc1mpt  48671  ackval1  48674  fuco21  49329  prcofval  49371  aacllem  49794