Theorem mpteq2dv 5205

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ↦ cmpt 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5174  df-mpt 5193

This theorem is referenced by:  ifmpt2v  7512  ofeqd  7676  mpocurryvald  8262  rdgeq1  8394  rdgeq2  8395  omv  8493  oev  8495  oieq1  9470  oieq2  9471  cantnflem1  9654  wunex2  10718  wuncval2  10727  indval  12216  rpnnen1  13002  seqof2  14092  relexpsucnnr  15058  relexp1g  15059  limsupval  15521  sumeq2w  15739  sumeq2ii  15740  cbvsum  15742  cbvsumv  15743  sumeq2sdv  15750  summo  15764  fsum  15767  fsumrlim  15859  fsumo1  15860  prodeq1  15957  prodeq2w  15960  prodeq2sdv  15973  prodmo  15986  fprod  15991  bpolylem  16097  rpnnen2lem1  16265  rpnnen2lem2  16266  1arithlem1  16978  vdwapval  17028  vdwlem6  17041  vdwlem8  17043  vdwlem9  17044  vdwlem10  17045  ramub1lem2  17082  ramcl  17084  sloteq  17238  prdsplusgval  17521  prdsmulrval  17523  prdsdsval  17526  prdsvscaval  17527  ismon  17785  fucco  18017  curf1  18276  curf2  18280  yonedalem4a  18326  smndex1gbas  18956  smndex1gbasOLD  18957  smndex1gid  18958  smndex1gidOLD  18959  smndex1igid  18960  grplactfval  19102  galactghm  19469  pmtrval  19516  sylow1  19668  sylow2b  19688  sylow3lem5  19696  sylow3  19698  iscyg  19944  gsumzaddlem  19986  gsumzmhm  20002  ablfac2  20156  gsumdixp  20396  c0rhm  20633  c0rnghm  20634  zncyg  21698  phllmhm  21782  isphld  21804  frlmgsum  21922  frlmipval  21929  frlmphl  21931  uvcval  21935  fczpsrbag  22071  psrmulfval  22093  psrascl  22128  mvrval  22131  subrgmvr  22184  mplcoe1  22188  mplcoe3  22189  mplcoe5  22191  mplmon2  22212  subrgascl  22217  evlslem2  22230  evlslem3  22231  evlslem1  22233  mpfrcl  22236  evlsval  22237  evlsvval  22241  evlsvvval  22244  evlsvar  22246  mpfind  22266  selvfval  22270  selvval  22271  selvvvval  22293  mhpfval  22301  psdfval  22321  psdval  22322  psdmvr  22332  coe1fval  22365  pf1ind  22515  evl1gsumadd  22518  rhmmpl  22540  rhmply1vr1  22544  mamuval  22550  mamufv  22551  matgsum  22594  madetsumid  22618  mat1dimmul  22633  mvmulval  22700  mvmulfv  22701  mavmulfv  22703  1mavmul  22705  marepvval0  22723  mulmarep1gsum1  22730  mdetleib  22744  mdetleib2  22745  mdetfval1  22747  mdetleib1  22748  mdet0pr  22749  m1detdiag  22754  mdetralt  22765  mdetunilem9  22777  m2detleib  22788  smadiadetlem3  22825  mat2pmatmul  22888  decpmatmul  22929  decpmatmulsumfsupp  22930  pmatcollpw1  22933  monmatcollpw  22936  pmatcollpw3lem  22940  pmatcollpw3fi1lem2  22944  pm2mpval  22952  pm2mpfval  22953  mply1topmatval  22961  mp2pm2mplem1  22963  mp2pm2mplem3  22965  ptbasfi  23738  ptcnplem  23778  ptrescn  23796  cnmpt2k  23845  xkohmeo  23972  fmval  24100  fmf  24102  ptcmpg  24214  tmdmulg  24249  prdstmdd  24281  tsmspropd  24289  prdsxmslem2  24686  metdsval  25005  fsumcn  25029  expcn  25031  lebnumlem3  25122  pcoval  25170  pi1xfrcnv  25216  cphsscph  25410  rrxds  25552  rrxmval  25564  itg11  25850  mbfi1fseqlem2  25875  mbfi1fseqlem6  25879  mbfi1fseq  25880  mbfi1flimlem  25881  mbfmullem  25884  itg2const  25899  itg2mulc  25906  itg2monolem1  25909  itg2i1fseqle  25913  itg2i1fseq  25914  itg2addlem  25917  itg2cnlem1  25920  itg2cn  25922  isibl  25924  isibl2  25925  iblitg  25927  itgeq1  25932  itgz  25940  itgvallem  25944  itgvallem3  25945  iblcnlem1  25947  itgcnlem  25949  iblrelem  25950  iblposlem  25951  iblpos  25952  itgrevallem1  25954  itgposval  25955  iblss2  25965  itgss  25971  itgfsum  25986  iblabslem  25987  iblmulc2  25990  bddmulibl  25998  itgcn  26004  ellimc  26032  dvnfval  26081  cpnfval  26091  dvexp  26112  dvexp2  26113  dvmptfsum  26134  dvlipcn  26153  dvivthlem1  26167  dvfsumle  26180  dvfsumabs  26182  dvfsumlem2  26186  itgpowd  26209  elply2  26353  elplyr  26358  elplyd  26359  coeeu  26382  coelem  26383  coeeq  26384  plyco  26398  coe11  26410  coe1termlem  26415  dgrcolem1  26430  dvply2g  26446  elqaalem3  26482  eltayl  26523  tayl0  26525  taylthlem1  26536  taylthlem2  26537  ulmcau  26558  ulmdvlem1  26563  ulmdvlem3  26565  mtest  26567  mtestbdd  26568  pserval  26573  pserulm  26585  psercn  26589  pserdvlem2  26591  abelthlem3  26596  logtayl  26825  dvcxp1  26905  dvcncxp1  26908  logbmpt  26953  dmarea  27122  lgamgulmlem2  27194  lgamgulmlem5  27197  musum  27355  dchrptlem2  27429  dchrptlem3  27430  dchrpt  27431  lgsval  27465  lgsval4lem  27472  lgsneg  27485  lgsmod  27487  rpvmasum2  27676  padicfval  27780  ostth2  27801  ostth3  27802  ostth  27803  lmif  29094  islmib  29096  incistruhgr  29429  eucrct2eupth  30596  htthlem  31269  htth  31270  pjhfval  31748  hosmval  32087  hommval  32088  hodmval  32089  hfsmval  32090  hfmmval  32091  brafval  32295  kbfval  32304  mptprop  33043  indsn  33183  psgnfzto1st  33425  fxpsubm  33492  fxpsubg  33493  fxpsubrg  33494  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem3  33564  elrgspnlem4  33565  elrgspn  33566  elrgspnsubrunlem1  33567  linds2eq  33694  elrspunidl  33736  elrspunsn  33737  evl1deg1  33866  evl1deg2  33867  evl1deg3  33868  mplasclco  33906  selvply1rhmlema  33908  selvply1rhmlemb  33909  selvply1rhmlem2  33911  selvply1rhmlem3  33912  selvply1rhmlem4  33913  selvply1rhmlem5  33914  selvply1rhm  33915  mplidom  33918  extvfval  33922  extvfv  33923  mvrvalind  33928  evlextv  33932  mplvrpmfgalem  33934  mplvrpmga  33935  mplvrpmmhm  33936  mplvrpmrhm  33937  psrgsum  33938  psrmonmul2  33941  psrmonprod  33942  splysubrg  33950  issply  33951  esplyval  33952  esplyfvaln  33964  vietalem  33969  vieta  33970  lbsdiflsp0  34016  fedgmullem1  34019  fedgmullem2  34020  fedgmul  34021  evls1fldgencl  34060  fldextrspunlsplem  34063  fldextrspunlsp  34064  extdgfialglem2  34083  mdetpmtr1  34213  zar0ring  34268  ordtcnvNEW  34310  ordtrest2NEW  34313  xrhval  34408  esum2dlem  34482  ofceq  34487  itgeq12dv  34716  ballotlemfval  34880  vtsval  35024  lpadval  35066  ptpconn  35725  cvmliftlem15  35790  cvmlift2lem4  35798  cvmlift2  35808  snmlval  35823  snmlflim  35824  satf  35845  mrsubfval  36000  mrsubrn  36005  elmsubrn  36020  msubrn  36021  msubco  36023  faclim  36238  faclim2  36240  prodeq12sdv  36730  itgeq12sdv  36731  cbvsumdavw  36791  cbvproddavw  36792  cbvsumdavw2  36807  cbvproddavw2  36808  knoppcnlem1  37082  knoppcnlem6  37087  knoppcnlem7  37088  bj-evaleq  37713  csbrdgg  37975  curfv  38251  matunitlindflem2  38268  poimirlem5  38276  poimirlem6  38277  poimirlem7  38278  poimirlem8  38279  poimirlem10  38281  poimirlem11  38282  poimirlem12  38283  poimirlem15  38286  poimirlem16  38287  poimirlem17  38288  poimirlem18  38289  poimirlem19  38290  poimirlem20  38291  poimirlem21  38292  poimirlem22  38293  poimirlem27  38298  voliunnfl  38315  itg2addnclem  38322  itg2addnclem3  38324  itg2addnc  38325  itg2gt0cn  38326  iblabsnclem  38334  iblmulc2nc  38336  ftc1anclem2  38345  ftc1anclem6  38349  ftc1anclem8  38351  ftc1anc  38352  ftc2nc  38353  upixp  38380  rrncmslem  38483  ismrer1  38489  tendoplcbv  41549  tendopl  41550  tendoicbv  41567  tendoi  41568  dihfval  42005  lcfl7N  42275  lcfrlem8  42323  lcfrlem9  42324  lcf1o  42325  hvmapval  42534  hdmap1fval  42570  hdmapffval  42600  hdmapfval  42601  hgmapffval  42659  hgmapfval  42660  lcmineqlem7  42802  lcmineqlem12  42807  aks6d1c6lem5  42944  rhmpsr  43315  evlsbagval  43318  evlselv  43321  fsuppind  43322  fsuppssindlem2  43324  fsuppssind  43325  mzpclval  43456  mzpcl2  43461  mzpexpmpt  43476  mzpsubst  43479  mzpcompact2lem  43482  rmxfval  43631  rmyfval  43632  aomclem8  43788  hbtlem1  43850  hbtlem7  43852  rfovfvd  44728  fsovrfovd  44735  fsovfvd  44736  fsovcnvlem  44739  dssmapfv2d  44744  dssmapnvod  44746  ntrneibex  44799  mnringmulrvald  44951  mnringmulrcld  44952  expgrowthi  45043  expgrowth  45045  binomcxplemdvsum  45065  addrval  45174  subrval  45175  mulvval  45176  fmulcl  46297  fmuldfeqlem1  46298  fprodcnlem  46315  fprodcn  46316  fnlimfv  46377  fnlimcnv  46381  fnlimfvre  46388  fnlimfvre2  46391  fnlimf  46392  fnlimabslt  46393  liminfval  46473  limsupresxr  46480  liminfresxr  46481  liminfvalxr  46497  fprodcncf  46614  dvnmptdivc  46652  dvnxpaek  46656  dvnmul  46657  dvmptfprod  46659  dvnprodlem1  46660  dvnprodlem2  46661  dvnprodlem3  46662  dvnprod  46663  stoweidlem2  46716  stoweidlem17  46731  stoweidlem19  46733  stoweidlem20  46734  stoweidlem43  46757  stoweidlem62  46776  stoweid  46777  dirkercncflem2  46818  fourierdlem112  46932  fourierdlem113  46933  etransclem1  46949  etransclem5  46953  etransclem17  46965  etransclem19  46967  etransclem22  46970  sge0val  47080  ovnlecvr  47272  ovncvrrp  47278  ovn0lem  47279  ovnsubaddlem1  47284  ovnsubadd  47286  hsphoif  47290  hsphoival  47293  hoidmv1lelem1  47305  hoidmv1lelem2  47306  hoidmv1lelem3  47307  hoidmv1le  47308  hoidmvlelem1  47309  hoidmvlelem2  47310  hoidmvlelem3  47311  hoidmvlelem4  47312  hoidmvlelem5  47313  hoidmvle  47314  ovnhoilem1  47315  ovnhoi  47317  hoidifhspval  47322  ovncvr2  47325  hoidifhspval2  47329  hspmbllem2  47341  hspmbllem3  47342  hspmbl  47343  ovnovollem1  47370  vonioolem2  47395  vonioo  47396  vonicclem2  47398  vonicc  47399  smflimlem4  47488  smflim  47491  smflim2  47520  smfsuplem2  47526  smfsup  47528  smfinf  47532  smflimsuplem2  47535  smflimsuplem5  47538  smflimsuplem7  47540  smflimsup  47542  cfsetsnfsetfo  47797  lincop  49188  1arymaptfv  49420  itcoval  49441  itcovalpc  49452  itcovalt2  49457  ackvalsuc1mpt  49458  ackval1  49461  fuco21  50114  prcofval  50156  aacllem  50621