Theorem mpteq2dv 5194

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-mpt 5182

This theorem is referenced by:  ifmpt2v  7470  ofeqd  7634  mpocurryvald  8222  rdgeq1  8352  rdgeq2  8353  omv  8449  oev  8451  oieq1  9429  oieq2  9430  cantnflem1  9610  wunex2  10661  wuncval2  10670  rpnnen1  12908  seqof2  13995  relexpsucnnr  14960  relexp1g  14961  limsupval  15409  sumeq2w  15627  sumeq2ii  15628  cbvsum  15630  cbvsumv  15631  sumeq2sdv  15638  summo  15652  fsum  15655  fsumrlim  15746  fsumo1  15747  prodeq1  15842  prodeq2w  15845  prodeq2sdv  15858  prodmo  15871  fprod  15876  bpolylem  15983  rpnnen2lem1  16151  rpnnen2lem2  16152  1arithlem1  16863  vdwapval  16913  vdwlem6  16926  vdwlem8  16928  vdwlem9  16929  vdwlem10  16930  ramub1lem2  16967  ramcl  16969  sloteq  17122  prdsplusgval  17405  prdsmulrval  17407  prdsdsval  17410  prdsvscaval  17411  ismon  17669  fucco  17901  curf1  18160  curf2  18164  yonedalem4a  18210  smndex1gbas  18839  smndex1gid  18840  grplactfval  18983  galactghm  19345  pmtrval  19392  sylow1  19544  sylow2b  19564  sylow3lem5  19572  sylow3  19574  iscyg  19820  gsumzaddlem  19862  gsumzmhm  19878  ablfac2  20032  gsumdixp  20266  c0rhm  20479  c0rnghm  20480  zncyg  21515  phllmhm  21599  isphld  21621  frlmgsum  21739  frlmipval  21746  frlmphl  21748  uvcval  21752  fczpsrbag  21889  psrmulfval  21911  psrascl  21946  mvrval  21949  subrgmvr  22000  mplcoe1  22004  mplcoe3  22005  mplcoe5  22007  mplmon2  22028  subrgascl  22033  evlslem2  22046  evlslem3  22047  evlslem1  22049  mpfrcl  22052  evlsval  22053  evlsvval  22057  evlsvvval  22060  evlsvar  22062  mpfind  22082  selvfval  22089  selvval  22090  mhpfval  22093  psdfval  22113  psdval  22114  psdmvr  22124  coe1fval  22158  pf1ind  22311  evl1gsumadd  22314  rhmmpl  22339  rhmply1vr1  22343  mamuval  22349  mamufv  22350  matgsum  22393  madetsumid  22417  mat1dimmul  22432  mvmulval  22499  mvmulfv  22500  mavmulfv  22502  1mavmul  22504  marepvval0  22522  mulmarep1gsum1  22529  mdetleib  22543  mdetleib2  22544  mdetfval1  22546  mdetleib1  22547  mdet0pr  22548  m1detdiag  22553  mdetralt  22564  mdetunilem9  22576  m2detleib  22587  smadiadetlem3  22624  mat2pmatmul  22687  decpmatmul  22728  decpmatmulsumfsupp  22729  pmatcollpw1  22732  monmatcollpw  22735  pmatcollpw3lem  22739  pmatcollpw3fi1lem2  22743  pm2mpval  22751  pm2mpfval  22752  mply1topmatval  22760  mp2pm2mplem1  22762  mp2pm2mplem3  22764  ptbasfi  23537  ptcnplem  23577  ptrescn  23595  cnmpt2k  23644  xkohmeo  23771  fmval  23899  fmf  23901  ptcmpg  24013  tmdmulg  24048  prdstmdd  24080  tsmspropd  24088  prdsxmslem2  24485  metdsval  24804  fsumcn  24829  expcn  24831  expcnOLD  24833  lebnumlem3  24930  pcoval  24979  pi1xfrcnv  25025  cphsscph  25219  rrxds  25361  rrxmval  25373  itg11  25660  mbfi1fseqlem2  25685  mbfi1fseqlem6  25689  mbfi1fseq  25690  mbfi1flimlem  25691  mbfmullem  25694  itg2const  25709  itg2mulc  25716  itg2monolem1  25719  itg2i1fseqle  25723  itg2i1fseq  25724  itg2addlem  25727  itg2cnlem1  25730  itg2cn  25732  isibl  25734  isibl2  25735  iblitg  25737  itgeq1  25742  itgz  25750  itgvallem  25754  itgvallem3  25755  iblcnlem1  25757  itgcnlem  25759  iblrelem  25760  iblposlem  25761  iblpos  25762  itgrevallem1  25764  itgposval  25765  iblss2  25775  itgss  25781  itgfsum  25796  iblabslem  25797  iblmulc2  25800  bddmulibl  25808  itgcn  25814  ellimc  25842  dvnfval  25892  cpnfval  25902  dvexp  25925  dvexp2  25926  dvmptfsum  25947  dvlipcn  25967  dvivthlem1  25981  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  itgpowd  26025  elply2  26169  elplyr  26174  elplyd  26175  coeeu  26198  coelem  26199  coeeq  26200  plyco  26214  coe11  26226  coe1termlem  26231  dgrcolem1  26247  dvply2g  26260  dvply2gOLD  26261  elqaalem3  26297  eltayl  26335  tayl0  26337  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmcau  26372  ulmdvlem1  26377  ulmdvlem3  26379  mtest  26381  mtestbdd  26382  pserval  26387  pserulm  26399  psercn  26404  pserdvlem2  26406  abelthlem3  26411  logtayl  26637  dvcxp1  26717  dvcncxp1  26720  logbmpt  26766  dmarea  26935  lgamgulmlem2  27008  lgamgulmlem5  27011  musum  27169  dchrptlem2  27244  dchrptlem3  27245  dchrpt  27246  lgsval  27280  lgsval4lem  27287  lgsneg  27300  lgsmod  27302  rpvmasum2  27491  padicfval  27595  ostth2  27616  ostth3  27617  ostth  27618  lmif  28869  islmib  28871  incistruhgr  29164  eucrct2eupth  30332  htthlem  31005  htth  31006  pjhfval  31484  hosmval  31823  hommval  31824  hodmval  31825  hfsmval  31826  hfmmval  31827  brafval  32031  kbfval  32040  mptprop  32788  indval  32943  indsn  32956  psgnfzto1st  33199  fxpsubm  33266  fxpsubg  33267  fxpsubrg  33268  elrgspnlem1  33336  elrgspnlem2  33337  elrgspnlem3  33338  elrgspnlem4  33339  elrgspn  33340  elrgspnsubrunlem1  33341  linds2eq  33474  elrspunidl  33521  elrspunsn  33522  evl1deg1  33669  evl1deg2  33670  evl1deg3  33671  extvfval  33709  extvfv  33710  mvrvalind  33715  evlextv  33719  mplvrpmfgalem  33721  mplvrpmga  33722  mplvrpmmhm  33723  mplvrpmrhm  33724  psrgsum  33725  psrmonmul2  33728  psrmonprod  33729  splysubrg  33737  issply  33738  esplyval  33739  esplyfvaln  33751  vietalem  33756  vieta  33757  lbsdiflsp0  33804  fedgmullem1  33807  fedgmullem2  33808  fedgmul  33809  evls1fldgencl  33848  fldextrspunlsplem  33851  fldextrspunlsp  33852  extdgfialglem2  33871  mdetpmtr1  34001  zar0ring  34056  ordtcnvNEW  34098  ordtrest2NEW  34101  xrhval  34196  esum2dlem  34270  ofceq  34275  itgeq12dv  34504  ballotlemfval  34668  vtsval  34815  lpadval  34854  ptpconn  35449  cvmliftlem15  35514  cvmlift2lem4  35522  cvmlift2  35532  snmlval  35547  snmlflim  35548  satf  35569  mrsubfval  35724  mrsubrn  35729  elmsubrn  35744  msubrn  35745  msubco  35747  faclim  35962  faclim2  35964  prodeq12sdv  36434  itgeq12sdv  36435  cbvsumdavw  36495  cbvproddavw  36496  cbvsumdavw2  36511  cbvproddavw2  36512  knoppcnlem1  36715  knoppcnlem6  36720  knoppcnlem7  36721  bj-evaleq  37324  csbrdgg  37584  curfv  37851  matunitlindflem2  37868  poimirlem5  37876  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem10  37881  poimirlem11  37882  poimirlem12  37883  poimirlem15  37886  poimirlem16  37887  poimirlem17  37888  poimirlem18  37889  poimirlem19  37890  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  poimirlem27  37898  voliunnfl  37915  itg2addnclem  37922  itg2addnclem3  37924  itg2addnc  37925  itg2gt0cn  37926  iblabsnclem  37934  iblmulc2nc  37936  ftc1anclem2  37945  ftc1anclem6  37949  ftc1anclem8  37951  ftc1anc  37952  ftc2nc  37953  upixp  37980  rrncmslem  38083  ismrer1  38089  tendoplcbv  41151  tendopl  41152  tendoicbv  41169  tendoi  41170  dihfval  41607  lcfl7N  41877  lcfrlem8  41925  lcfrlem9  41926  lcf1o  41927  hvmapval  42136  hdmap1fval  42172  hdmapffval  42202  hdmapfval  42203  hgmapffval  42261  hgmapfval  42262  lcmineqlem7  42405  lcmineqlem12  42410  aks6d1c6lem5  42547  rhmpsr  42920  evlsbagval  42927  selvvvval  42943  evlselv  42945  fsuppind  42948  fsuppssindlem2  42950  fsuppssind  42951  mzpclval  43082  mzpcl2  43087  mzpexpmpt  43102  mzpsubst  43105  mzpcompact2lem  43108  rmxfval  43261  rmyfval  43262  aomclem8  43418  hbtlem1  43480  hbtlem7  43482  rfovfvd  44358  fsovrfovd  44365  fsovfvd  44366  fsovcnvlem  44369  dssmapfv2d  44374  dssmapnvod  44376  ntrneibex  44429  mnringmulrvald  44583  mnringmulrcld  44584  expgrowthi  44689  expgrowth  44691  binomcxplemdvsum  44711  addrval  44821  subrval  44822  mulvval  44823  fmulcl  45941  fmuldfeqlem1  45942  fprodcnlem  45959  fprodcn  45960  fnlimfv  46021  fnlimcnv  46025  fnlimfvre  46032  fnlimfvre2  46035  fnlimf  46036  fnlimabslt  46037  liminfval  46117  limsupresxr  46124  liminfresxr  46125  liminfvalxr  46141  fprodcncf  46258  dvnmptdivc  46296  dvnxpaek  46300  dvnmul  46301  dvmptfprod  46303  dvnprodlem1  46304  dvnprodlem2  46305  dvnprodlem3  46306  dvnprod  46307  stoweidlem2  46360  stoweidlem17  46375  stoweidlem19  46377  stoweidlem20  46378  stoweidlem43  46401  stoweidlem62  46420  stoweid  46421  dirkercncflem2  46462  fourierdlem112  46576  fourierdlem113  46577  etransclem1  46593  etransclem5  46597  etransclem17  46609  etransclem19  46611  etransclem22  46614  sge0val  46724  ovnlecvr  46916  ovncvrrp  46922  ovn0lem  46923  ovnsubaddlem1  46928  ovnsubadd  46930  hsphoif  46934  hsphoival  46937  hoidmv1lelem1  46949  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmv1le  46952  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem4  46956  hoidmvlelem5  46957  hoidmvle  46958  ovnhoilem1  46959  ovnhoi  46961  hoidifhspval  46966  ovncvr2  46969  hoidifhspval2  46973  hspmbllem2  46985  hspmbllem3  46986  hspmbl  46987  ovnovollem1  47014  vonioolem2  47039  vonioo  47040  vonicclem2  47042  vonicc  47043  smflimlem4  47132  smflim  47135  smflim2  47164  smfsuplem2  47170  smfsup  47172  smfinf  47176  smflimsuplem2  47179  smflimsuplem5  47182  smflimsuplem7  47184  smflimsup  47186  cfsetsnfsetfo  47420  lincop  48768  1arymaptfv  49000  itcoval  49021  itcovalpc  49032  itcovalt2  49037  ackvalsuc1mpt  49038  ackval1  49041  fuco21  49695  prcofval  49737  aacllem  50160