Theorem mpteq2dv 5180

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

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

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 5149  df-mpt 5168

This theorem is referenced by:  ifmpt2v  7462  ofeqd  7626  mpocurryvald  8213  rdgeq1  8343  rdgeq2  8344  omv  8440  oev  8442  oieq1  9420  oieq2  9421  cantnflem1  9601  wunex2  10652  wuncval2  10661  indval  12153  rpnnen1  12924  seqof2  14013  relexpsucnnr  14978  relexp1g  14979  limsupval  15427  sumeq2w  15645  sumeq2ii  15646  cbvsum  15648  cbvsumv  15649  sumeq2sdv  15656  summo  15670  fsum  15673  fsumrlim  15765  fsumo1  15766  prodeq1  15863  prodeq2w  15866  prodeq2sdv  15879  prodmo  15892  fprod  15897  bpolylem  16004  rpnnen2lem1  16172  rpnnen2lem2  16173  1arithlem1  16885  vdwapval  16935  vdwlem6  16948  vdwlem8  16950  vdwlem9  16951  vdwlem10  16952  ramub1lem2  16989  ramcl  16991  sloteq  17144  prdsplusgval  17427  prdsmulrval  17429  prdsdsval  17432  prdsvscaval  17433  ismon  17691  fucco  17923  curf1  18182  curf2  18186  yonedalem4a  18232  smndex1gbas  18861  smndex1gbasOLD  18862  smndex1gid  18863  smndex1gidOLD  18864  smndex1igid  18865  grplactfval  19008  galactghm  19370  pmtrval  19417  sylow1  19569  sylow2b  19589  sylow3lem5  19597  sylow3  19599  iscyg  19845  gsumzaddlem  19887  gsumzmhm  19903  ablfac2  20057  gsumdixp  20289  c0rhm  20502  c0rnghm  20503  zncyg  21538  phllmhm  21622  isphld  21644  frlmgsum  21762  frlmipval  21769  frlmphl  21771  uvcval  21775  fczpsrbag  21911  psrmulfval  21932  psrascl  21967  mvrval  21970  subrgmvr  22021  mplcoe1  22025  mplcoe3  22026  mplcoe5  22028  mplmon2  22049  subrgascl  22054  evlslem2  22067  evlslem3  22068  evlslem1  22070  mpfrcl  22073  evlsval  22074  evlsvval  22078  evlsvvval  22081  evlsvar  22083  mpfind  22103  selvfval  22110  selvval  22111  mhpfval  22114  psdfval  22134  psdval  22135  psdmvr  22145  coe1fval  22179  pf1ind  22330  evl1gsumadd  22333  rhmmpl  22358  rhmply1vr1  22362  mamuval  22368  mamufv  22369  matgsum  22412  madetsumid  22436  mat1dimmul  22451  mvmulval  22518  mvmulfv  22519  mavmulfv  22521  1mavmul  22523  marepvval0  22541  mulmarep1gsum1  22548  mdetleib  22562  mdetleib2  22563  mdetfval1  22565  mdetleib1  22566  mdet0pr  22567  m1detdiag  22572  mdetralt  22583  mdetunilem9  22595  m2detleib  22606  smadiadetlem3  22643  mat2pmatmul  22706  decpmatmul  22747  decpmatmulsumfsupp  22748  pmatcollpw1  22751  monmatcollpw  22754  pmatcollpw3lem  22758  pmatcollpw3fi1lem2  22762  pm2mpval  22770  pm2mpfval  22771  mply1topmatval  22779  mp2pm2mplem1  22781  mp2pm2mplem3  22783  ptbasfi  23556  ptcnplem  23596  ptrescn  23614  cnmpt2k  23663  xkohmeo  23790  fmval  23918  fmf  23920  ptcmpg  24032  tmdmulg  24067  prdstmdd  24099  tsmspropd  24107  prdsxmslem2  24504  metdsval  24823  fsumcn  24847  expcn  24849  lebnumlem3  24940  pcoval  24988  pi1xfrcnv  25034  cphsscph  25228  rrxds  25370  rrxmval  25382  itg11  25668  mbfi1fseqlem2  25693  mbfi1fseqlem6  25697  mbfi1fseq  25698  mbfi1flimlem  25699  mbfmullem  25702  itg2const  25717  itg2mulc  25724  itg2monolem1  25727  itg2i1fseqle  25731  itg2i1fseq  25732  itg2addlem  25735  itg2cnlem1  25738  itg2cn  25740  isibl  25742  isibl2  25743  iblitg  25745  itgeq1  25750  itgz  25758  itgvallem  25762  itgvallem3  25763  iblcnlem1  25765  itgcnlem  25767  iblrelem  25768  iblposlem  25769  iblpos  25770  itgrevallem1  25772  itgposval  25773  iblss2  25783  itgss  25789  itgfsum  25804  iblabslem  25805  iblmulc2  25808  bddmulibl  25816  itgcn  25822  ellimc  25850  dvnfval  25899  cpnfval  25909  dvexp  25930  dvexp2  25931  dvmptfsum  25952  dvlipcn  25971  dvivthlem1  25985  dvfsumle  25998  dvfsumabs  26000  dvfsumlem2  26004  itgpowd  26027  elply2  26171  elplyr  26176  elplyd  26177  coeeu  26200  coelem  26201  coeeq  26202  plyco  26216  coe11  26228  coe1termlem  26233  dgrcolem1  26248  dvply2g  26261  dvply2gOLD  26262  elqaalem3  26298  eltayl  26336  tayl0  26338  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  ulmcau  26373  ulmdvlem1  26378  ulmdvlem3  26380  mtest  26382  mtestbdd  26383  pserval  26388  pserulm  26400  psercn  26404  pserdvlem2  26406  abelthlem3  26411  logtayl  26637  dvcxp1  26717  dvcncxp1  26720  logbmpt  26765  dmarea  26934  lgamgulmlem2  27007  lgamgulmlem5  27010  musum  27168  dchrptlem2  27242  dchrptlem3  27243  dchrpt  27244  lgsval  27278  lgsval4lem  27285  lgsneg  27298  lgsmod  27300  rpvmasum2  27489  padicfval  27593  ostth2  27614  ostth3  27615  ostth  27616  lmif  28867  islmib  28869  incistruhgr  29162  eucrct2eupth  30330  htthlem  31003  htth  31004  pjhfval  31482  hosmval  31821  hommval  31822  hodmval  31823  hfsmval  31824  hfmmval  31825  brafval  32029  kbfval  32038  mptprop  32786  indsn  32938  psgnfzto1st  33181  fxpsubm  33248  fxpsubg  33249  fxpsubrg  33250  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  elrgspn  33322  elrgspnsubrunlem1  33323  linds2eq  33456  elrspunidl  33503  elrspunsn  33504  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  extvfval  33691  extvfv  33692  mvrvalind  33697  evlextv  33701  mplvrpmfgalem  33703  mplvrpmga  33704  mplvrpmmhm  33705  mplvrpmrhm  33706  psrgsum  33707  psrmonmul2  33710  psrmonprod  33711  splysubrg  33719  issply  33720  esplyval  33721  esplyfvaln  33733  vietalem  33738  vieta  33739  lbsdiflsp0  33786  fedgmullem1  33789  fedgmullem2  33790  fedgmul  33791  evls1fldgencl  33830  fldextrspunlsplem  33833  fldextrspunlsp  33834  extdgfialglem2  33853  mdetpmtr1  33983  zar0ring  34038  ordtcnvNEW  34080  ordtrest2NEW  34083  xrhval  34178  esum2dlem  34252  ofceq  34257  itgeq12dv  34486  ballotlemfval  34650  vtsval  34797  lpadval  34836  ptpconn  35431  cvmliftlem15  35496  cvmlift2lem4  35504  cvmlift2  35514  snmlval  35529  snmlflim  35530  satf  35551  mrsubfval  35706  mrsubrn  35711  elmsubrn  35726  msubrn  35727  msubco  35729  faclim  35944  faclim2  35946  prodeq12sdv  36416  itgeq12sdv  36417  cbvsumdavw  36477  cbvproddavw  36478  cbvsumdavw2  36493  cbvproddavw2  36494  knoppcnlem1  36769  knoppcnlem6  36774  knoppcnlem7  36775  bj-evaleq  37399  csbrdgg  37659  curfv  37935  matunitlindflem2  37952  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem27  37982  voliunnfl  37999  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  itg2gt0cn  38010  iblabsnclem  38018  iblmulc2nc  38020  ftc1anclem2  38029  ftc1anclem6  38033  ftc1anclem8  38035  ftc1anc  38036  ftc2nc  38037  upixp  38064  rrncmslem  38167  ismrer1  38173  tendoplcbv  41235  tendopl  41236  tendoicbv  41253  tendoi  41254  dihfval  41691  lcfl7N  41961  lcfrlem8  42009  lcfrlem9  42010  lcf1o  42011  hvmapval  42220  hdmap1fval  42256  hdmapffval  42286  hdmapfval  42287  hgmapffval  42345  hgmapfval  42346  lcmineqlem7  42488  lcmineqlem12  42493  aks6d1c6lem5  42630  rhmpsr  43009  evlsbagval  43016  selvvvval  43032  evlselv  43034  fsuppind  43037  fsuppssindlem2  43039  fsuppssind  43040  mzpclval  43171  mzpcl2  43176  mzpexpmpt  43191  mzpsubst  43194  mzpcompact2lem  43197  rmxfval  43350  rmyfval  43351  aomclem8  43507  hbtlem1  43569  hbtlem7  43571  rfovfvd  44447  fsovrfovd  44454  fsovfvd  44455  fsovcnvlem  44458  dssmapfv2d  44463  dssmapnvod  44465  ntrneibex  44518  mnringmulrvald  44672  mnringmulrcld  44673  expgrowthi  44778  expgrowth  44780  binomcxplemdvsum  44800  addrval  44910  subrval  44911  mulvval  44912  fmulcl  46029  fmuldfeqlem1  46030  fprodcnlem  46047  fprodcn  46048  fnlimfv  46109  fnlimcnv  46113  fnlimfvre  46120  fnlimfvre2  46123  fnlimf  46124  fnlimabslt  46125  liminfval  46205  limsupresxr  46212  liminfresxr  46213  liminfvalxr  46229  fprodcncf  46346  dvnmptdivc  46384  dvnxpaek  46388  dvnmul  46389  dvmptfprod  46391  dvnprodlem1  46392  dvnprodlem2  46393  dvnprodlem3  46394  dvnprod  46395  stoweidlem2  46448  stoweidlem17  46463  stoweidlem19  46465  stoweidlem20  46466  stoweidlem43  46489  stoweidlem62  46508  stoweid  46509  dirkercncflem2  46550  fourierdlem112  46664  fourierdlem113  46665  etransclem1  46681  etransclem5  46685  etransclem17  46697  etransclem19  46699  etransclem22  46702  sge0val  46812  ovnlecvr  47004  ovncvrrp  47010  ovn0lem  47011  ovnsubaddlem1  47016  ovnsubadd  47018  hsphoif  47022  hsphoival  47025  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1lelem3  47039  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hoidmvlelem5  47045  hoidmvle  47046  ovnhoilem1  47047  ovnhoi  47049  hoidifhspval  47054  ovncvr2  47057  hoidifhspval2  47061  hspmbllem2  47073  hspmbllem3  47074  hspmbl  47075  ovnovollem1  47102  vonioolem2  47127  vonioo  47128  vonicclem2  47130  vonicc  47131  smflimlem4  47220  smflim  47223  smflim2  47252  smfsuplem2  47258  smfsup  47260  smfinf  47264  smflimsuplem2  47267  smflimsuplem5  47270  smflimsuplem7  47272  smflimsup  47274  cfsetsnfsetfo  47520  lincop  48896  1arymaptfv  49128  itcoval  49149  itcovalpc  49160  itcovalt2  49165  ackvalsuc1mpt  49166  ackval1  49169  fuco21  49823  prcofval  49865  aacllem  50288