Theorem mpteq2dv 5126

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-opab 5093  df-mpt 5111

This theorem is referenced by:  ofeq  7391  mpocurryvald  7919  rdgeq1  8030  rdgeq2  8031  omv  8120  oev  8122  oieq1  8960  oieq2  8961  cantnflem1  9136  wunex2  10149  wuncval2  10158  rpnnen1  12370  seqof2  13424  relexpsucnnr  14376  relexp1g  14377  limsupval  14823  sumeq2w  15041  sumeq2ii  15042  cbvsum  15044  summo  15066  fsum  15069  fsumrlim  15158  fsumo1  15159  prodeq2w  15258  prodmo  15282  fprod  15287  bpolylem  15394  rpnnen2lem1  15559  rpnnen2lem2  15560  1arithlem1  16249  vdwapval  16299  vdwlem6  16312  vdwlem8  16314  vdwlem9  16315  vdwlem10  16316  ramub1lem2  16353  ramcl  16355  sloteq  16480  prdsplusgval  16738  prdsmulrval  16740  prdsdsval  16743  prdsvscaval  16744  ismon  16995  fucco  17224  curf1  17467  curf2  17471  yonedalem4a  17517  smndex1gbas  18059  smndex1gid  18060  grplactfval  18192  galactghm  18524  pmtrval  18571  sylow1  18720  sylow2b  18740  sylow3lem5  18748  sylow3  18750  iscyg  18991  gsumzaddlem  19034  gsumzmhm  19050  ablfac2  19204  gsumdixp  19355  zncyg  20240  phllmhm  20321  isphld  20343  frlmgsum  20461  frlmipval  20468  frlmphl  20470  uvcval  20474  fczpsrbag  20605  psrmulfval  20623  mvrval  20659  subrgmvr  20701  mplcoe1  20705  mplcoe3  20706  mplcoe5  20708  mplmon2  20732  subrgascl  20737  evlslem2  20751  evlslem3  20752  evlslem1  20754  mpfrcl  20757  evlsval  20758  evlsvar  20762  mpfind  20779  selvfval  20789  selvval  20790  mhpfval  20791  coe1fval  20834  pf1ind  20979  evl1gsumadd  20982  mamuval  20993  mamufv  20994  matgsum  21042  madetsumid  21066  mat1dimmul  21081  mvmulval  21148  mvmulfv  21149  mavmulfv  21151  1mavmul  21153  marepvval0  21171  mulmarep1gsum1  21178  mdetleib  21192  mdetleib2  21193  mdetfval1  21195  mdetleib1  21196  mdet0pr  21197  m1detdiag  21202  mdetralt  21213  mdetunilem9  21225  m2detleib  21236  smadiadetlem3  21273  mat2pmatmul  21336  decpmatmul  21377  decpmatmulsumfsupp  21378  pmatcollpw1  21381  monmatcollpw  21384  pmatcollpw3lem  21388  pmatcollpw3fi1lem2  21392  pm2mpval  21400  pm2mpfval  21401  mply1topmatval  21409  mp2pm2mplem1  21411  mp2pm2mplem3  21413  ptbasfi  22186  ptcnplem  22226  ptrescn  22244  cnmpt2k  22293  xkohmeo  22420  fmval  22548  fmf  22550  ptcmpg  22662  tmdmulg  22697  prdstmdd  22729  tsmspropd  22737  prdsxmslem2  23136  metdsval  23452  fsumcn  23475  expcn  23477  lebnumlem3  23568  pcoval  23616  pi1xfrcnv  23662  cphsscph  23855  rrxds  23997  rrxmval  24009  itg11  24295  mbfi1fseqlem2  24320  mbfi1fseqlem6  24324  mbfi1fseq  24325  mbfi1flimlem  24326  mbfmullem  24329  itg2const  24344  itg2mulc  24351  itg2monolem1  24354  itg2i1fseqle  24358  itg2i1fseq  24359  itg2addlem  24362  itg2cnlem1  24365  itg2cn  24367  isibl  24369  isibl2  24370  iblitg  24372  itgz  24384  itgvallem  24388  itgvallem3  24389  iblcnlem1  24391  itgcnlem  24393  iblrelem  24394  iblposlem  24395  iblpos  24396  itgrevallem1  24398  itgposval  24399  iblss2  24409  itgss  24415  itgfsum  24430  iblabslem  24431  iblmulc2  24434  bddmulibl  24442  itgcn  24448  ellimc  24476  dvnfval  24525  cpnfval  24535  dvexp  24556  dvexp2  24557  dvmptfsum  24578  dvlipcn  24597  dvivthlem1  24611  dvfsumle  24624  dvfsumabs  24626  dvfsumlem2  24630  itgpowd  24653  elply2  24793  elplyr  24798  elplyd  24799  coeeu  24822  coelem  24823  coeeq  24824  plyco  24838  coe11  24850  coe1termlem  24855  dgrcolem1  24870  dvply2g  24881  elqaalem3  24917  eltayl  24955  tayl0  24957  taylthlem1  24968  taylthlem2  24969  ulmcau  24990  ulmdvlem1  24995  ulmdvlem3  24997  mtest  24999  mtestbdd  25000  pserval  25005  pserulm  25017  psercn  25021  pserdvlem2  25023  abelthlem3  25028  logtayl  25251  dvcxp1  25329  dvcncxp1  25332  logbmpt  25374  dmarea  25543  lgamgulmlem2  25615  lgamgulmlem5  25618  musum  25776  dchrptlem2  25849  dchrptlem3  25850  dchrpt  25851  lgsval  25885  lgsval4lem  25892  lgsneg  25905  lgsmod  25907  rpvmasum2  26096  padicfval  26200  ostth2  26221  ostth3  26222  ostth  26223  lmif  26579  islmib  26581  incistruhgr  26872  eucrct2eupth  28030  htthlem  28700  htth  28701  pjhfval  29179  hosmval  29518  hommval  29519  hodmval  29520  hfsmval  29521  hfmmval  29522  brafval  29726  kbfval  29735  mptprop  30458  psgnfzto1st  30797  linds2eq  30995  elrspunidl  31014  lbsdiflsp0  31110  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  mdetpmtr1  31176  zar0ring  31231  ordtcnvNEW  31273  ordtrest2NEW  31276  xrhval  31369  indval  31382  esum2dlem  31461  ofceq  31466  itgeq12dv  31694  ballotlemfval  31857  vtsval  32018  lpadval  32057  ptpconn  32593  cvmliftlem15  32658  cvmlift2lem4  32666  cvmlift2  32676  snmlval  32691  snmlflim  32692  satf  32713  mrsubfval  32868  mrsubrn  32873  elmsubrn  32888  msubrn  32889  msubco  32891  faclim  33091  faclim2  33093  trpredeq1  33172  trpredeq2  33173  knoppcnlem1  33945  knoppcnlem6  33950  knoppcnlem7  33951  bj-evaleq  34487  csbrdgg  34746  curfv  35037  matunitlindflem2  35054  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem27  35084  voliunnfl  35101  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  iblabsnclem  35120  iblmulc2nc  35122  ftc1anclem2  35131  ftc1anclem6  35135  ftc1anclem8  35137  ftc1anc  35138  ftc2nc  35139  upixp  35167  rrncmslem  35270  ismrer1  35276  tendoplcbv  38071  tendopl  38072  tendoicbv  38089  tendoi  38090  dihfval  38527  lcfl7N  38797  lcfrlem8  38845  lcfrlem9  38846  lcf1o  38847  hvmapval  39056  hdmap1fval  39092  hdmapffval  39122  hdmapfval  39123  hgmapffval  39181  hgmapfval  39182  lcmineqlem7  39323  lcmineqlem12  39328  fsuppind  39456  fsuppssindlem2  39458  fsuppssind  39459  mzpclval  39666  mzpcl2  39671  mzpexpmpt  39686  mzpsubst  39689  mzpcompact2lem  39692  rmxfval  39845  rmyfval  39846  aomclem8  40005  hbtlem1  40067  hbtlem7  40069  rfovfvd  40703  fsovrfovd  40710  fsovfvd  40711  fsovcnvlem  40714  dssmapfv2d  40719  dssmapnvod  40721  ntrneibex  40776  mnringmulrvald  40935  mnringmulrcld  40936  expgrowthi  41037  expgrowth  41039  binomcxplemdvsum  41059  addrval  41170  subrval  41171  mulvval  41172  fmulcl  42223  fmuldfeqlem1  42224  fprodcnlem  42241  fprodcn  42242  fnlimfv  42305  fnlimcnv  42309  fnlimfvre  42316  fnlimfvre2  42319  fnlimf  42320  fnlimabslt  42321  liminfval  42401  limsupresxr  42408  liminfresxr  42409  liminfvalxr  42425  fprodcncf  42542  dvnmptdivc  42580  dvnxpaek  42584  dvnmul  42585  dvmptfprod  42587  dvnprodlem1  42588  dvnprodlem2  42589  dvnprodlem3  42590  dvnprod  42591  stoweidlem2  42644  stoweidlem17  42659  stoweidlem19  42661  stoweidlem20  42662  stoweidlem43  42685  stoweidlem62  42704  stoweid  42705  dirkercncflem2  42746  fourierdlem112  42860  fourierdlem113  42861  etransclem1  42877  etransclem5  42881  etransclem17  42893  etransclem19  42895  etransclem22  42898  sge0val  43005  ovnlecvr  43197  ovncvrrp  43203  ovn0lem  43204  ovnsubaddlem1  43209  ovnsubadd  43211  hsphoif  43215  hsphoival  43218  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1lelem3  43232  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  hoidmvlelem5  43238  hoidmvle  43239  ovnhoilem1  43240  ovnhoi  43242  hoidifhspval  43247  ovncvr2  43250  hoidifhspval2  43254  hspmbllem2  43266  hspmbllem3  43267  hspmbl  43268  ovnovollem1  43295  vonioolem2  43320  vonioo  43321  vonicclem2  43323  vonicc  43324  smflimlem4  43407  smflim  43410  smflim2  43437  smfsuplem2  43443  smfsup  43445  smfinf  43449  smflimsuplem2  43452  smflimsuplem5  43455  smflimsuplem7  43457  smflimsup  43459  c0rhm  44536  c0rnghm  44537  lincop  44817  1arymaptfv  45054  itcoval  45075  itcovalpc  45086  itcovalt2  45091  ackvalsuc1mpt  45092  ackval1  45095  aacllem  45329