Theorem mpteq2dva 4744

Description: Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.)

Hypothesis

Ref	Expression
mpteq2dva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2dva	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dva

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq2da 4743	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ↦ cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-opab 4713  df-mpt 4730

This theorem is referenced by:  mpteq2dv  4745  2fvcoidd  6552  offval  6904  offval2  6914  caofinvl  6924  caofcom  6929  caofass  6931  caofdi  6933  caofdir  6934  caonncan  6935  curry1  7269  curry2  7272  mpt2curryd  7395  pw2f1olem  8064  mapxpen  8126  xpmapenlem  8127  cantnfp1  8578  cantnflem1d  8585  cantnflem1  8586  cnfcom2lem  8598  dfac12lem1  8965  seqof  12858  seqof2  12859  swrd0val  13421  swrdswrd  13460  repswswrd  13531  repswrevw  13533  revco  13580  ccatco  13581  repsco  13585  ofccat  13708  lo1eq  14299  rlimeq  14300  lo1mul2  14359  o1dif  14360  lo1sub  14361  rlimdiv  14376  caucvgr  14406  sumeq1  14419  fsumrlim  14543  fsumo1  14544  climfsum  14552  geomulcvg  14607  vdwlem8  15692  prmgapprmo  15766  restid2  16091  pwsplusgval  16150  pwsmulrval  16151  pwsvscafval  16154  qusin  16204  xpsaddlem  16235  xpsvsca  16239  catidd  16341  fuclid  16626  fucrid  16627  fucass  16628  setcepi  16738  prf1st  16844  prf2nd  16845  1st2ndprf  16846  curfcl  16872  curfuncf  16878  diag2  16885  curf2ndf  16887  hof2val  16896  hofcllem  16898  hofcl  16899  yonedalem4a  16915  yonedalem4c  16917  yonedalem3b  16919  yonedainv  16921  yonffthlem  16922  prdsidlem  17322  prdsmndd  17323  pwsco2mhm  17371  frmdup3lem  17403  frmdup3  17404  grpinvpropd  17490  prdsinvlem  17524  pwsinvg  17528  pwssub  17529  galactghm  17823  cayleylem1  17832  pmtrprfval  17907  sylow1lem2  18014  sylow3lem1  18042  efginvrel1  18141  frgpup3lem  18190  frgpup3  18191  prdscmnd  18264  iscyggen  18282  gsumval3  18308  gsumcllem  18309  gsumzsplit  18327  gsumsub  18348  gsummptf1o  18362  gsum2d  18371  gsum2d2  18373  gsumxp  18375  prdsgsum  18377  telgsumfz  18387  telgsumfz0  18389  telgsum  18391  dprdfsub  18420  dprdfeq0  18421  dprddisj2  18438  dprd2d2  18443  dpjidcl  18457  ablfaclem2  18485  ablfac2  18488  srgbinomlem3  18542  srgbinomlem4  18543  srgbinomlem  18544  gsumdixp  18609  prdsmgp  18610  prdsringd  18612  prdslmodd  18969  asclpropd  19346  psrass1lem  19377  psrlinv  19397  psrass1  19405  psrdi  19406  psrdir  19407  psrass23l  19408  psrcom  19409  psrass23  19410  resspsrmul  19417  mplsubrglem  19439  mplmonmul  19464  mplcoe1  19465  mplcoe5  19468  mplcoe4  19503  evlslem3  19514  evlslem1  19515  psrplusgpropd  19606  psropprmul  19608  coe1mul2  19639  coe1tm  19643  coe1tmmul2  19646  coe1tmmul  19647  coe1pwmul  19649  cply1mul  19664  ply1coe  19666  eqcoe1ply1eq  19667  lply1binomsc  19677  evl1gsummon  19729  mulgrhm2  19847  frgpcyg  19922  evpmodpmf1o  19942  phlpropd  20000  frlmphl  20120  uvcresum  20132  frlmup1  20137  mamures  20196  grpvrinv  20202  mhmvlin  20203  mamuass  20208  mamudi  20209  mamudir  20210  mamuvs1  20211  mamuvs2  20212  mpt2matmul  20252  mamutpos  20264  madetsumid  20267  dmatmul  20303  scmatscm  20319  1mavmul  20354  mavmulass  20355  mvmumamul1  20360  mulmarep1gsum1  20379  mulmarep1gsum2  20380  mdetleib2  20394  mdetfval1  20396  mdet0pr  20398  mdetdiag  20405  mdetdiagid  20406  mdetrlin  20408  mdetrsca  20409  mdetralt  20414  mdetunilem9  20426  gsummatr01  20465  smadiadetlem1a  20469  smadiadetlem3  20474  smadiadetlem4  20475  cpmatmcllem  20523  mat2pmatmul  20536  decpmatmullem  20576  decpmatmul  20577  pmatcollpw1lem2  20580  pmatcollpw  20586  pmatcollpw3lem  20588  pmatcollpwscmat  20596  idpm2idmp  20606  mp2pm2mplem3  20613  mp2pm2mplem4  20614  mp2pm2mplem5  20615  mp2pm2mp  20616  pm2mpghm  20621  pm2mpmhmlem2  20624  monmat2matmon  20629  pm2mp  20630  chpdmat  20646  chpscmat  20647  chpscmatgsumbin  20649  chpscmatgsummon  20650  chp0mat  20651  chpidmat  20652  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  chfacfpmmulgsum2  20670  cayhamlem1  20671  cpmidgsumm2pm  20674  cpmidpmat  20678  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  cpmadumatpoly  20688  cayhamlem3  20692  cayhamlem4  20693  cayleyhamilton0  20694  cayleyhamiltonALT  20696  neiptopnei  20936  neiptopreu  20937  ptcnplem  21424  cnmpt1t  21468  cnmpt12  21470  cnmptkp  21483  cnmptk1  21484  cnmpt1k  21485  cnmptkk  21486  cnmptk1p  21488  cnmpt2k  21491  qtopeu  21519  pt1hmeo  21609  ptunhmeo  21611  xkocnv  21617  xkohmeo  21618  flfcnp2  21811  cnmpt1plusg  21891  istgp2  21895  tmdmulg  21896  tgpmulg  21897  tmdgsum  21899  symgtgp  21905  subgtgp  21909  tgpconncomp  21916  prdstgpd  21928  tsmsmhm  21949  tsmsadd  21950  tsmssub  21952  tgptsmscls  21953  tsmssplit  21955  tsmsxplem1  21956  tsmsxplem2  21957  cnmpt1vsca  21997  tlmtgp  21999  ustuqtoplem  22043  utopsnneip  22052  ressprdsds  22176  metuval  22354  nmfval2  22395  tngnm  22455  nmoeq0  22540  idnghm  22547  cnmpt1ds  22645  fsumcn  22673  expcn  22675  divccn  22676  divccncf  22709  negcncf  22721  copco  22818  pcopt  22822  pcopt2  22823  pcoass  22824  pi1xfrcnvlem  22856  cnmpt1ip  23046  rrxnm  23179  rrxds  23181  minveclem3b  23199  divcncf  23216  ovolctb  23258  ovoliunnul  23275  voliunlem3  23320  ovolfs2  23339  uniioombllem2  23351  vitalilem4  23380  vitalilem5  23381  ismbf  23397  mbfss  23413  mbfmulc2re  23415  mbfneg  23417  mbfpos  23418  mbfposb  23420  mbfadd  23428  mbfsub  23429  mbfmulc2  23430  mbfinf  23432  mbflimsup  23433  mbflimlem  23434  i1fpos  23473  i1fposd  23474  itg1climres  23481  mbfmul  23493  itg2mulc  23514  itg2i1fseq  23522  itg2cnlem1  23528  itg2cnlem2  23529  itgresr  23545  iblneg  23569  i1fibl  23574  itgitg1  23575  iblsub  23588  itgfsum  23593  itgmulc2lem1  23598  limcmpt  23647  limccnp  23655  limcco  23657  dvreslem  23673  dvres2lem  23674  dvidlem  23679  dvcnp2  23683  dvaddbr  23701  dvmulbr  23702  dvmulf  23706  dvcmulf  23708  dvcobr  23709  dvcof  23711  dvcjbr  23712  dvcj  23713  dvfre  23714  dvexp  23716  dvexp2  23717  dvrec  23718  dvmptcmul  23727  dvmptdivc  23728  dvmptneg  23729  dvmptsub  23730  dvmptre  23732  dvmptim  23733  dvrecg  23736  dvmptdiv  23737  dvmptfsum  23738  dvcnvlem  23739  dvcnv  23740  dvexp3  23741  dvef  23743  dvsincos  23744  dv11cn  23764  lhop2  23778  lhop  23779  ftc2  23807  itgparts  23810  itgsubstlem  23811  mdegfval  23822  mdegmullem  23838  ply1termlem  23959  plypow  23961  plyconst  23962  plyeq0lem  23966  plypf1  23968  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  coeidlem  23993  plyco  23997  coeeq2  23998  0dgr  24001  0dgrb  24002  dgrcolem1  24029  dgrcolem2  24030  plycjlem  24032  dvply1  24039  dvply2g  24040  plydiveu  24053  plyremlem  24059  elqaalem3  24076  taylfval  24113  dvtaylp  24124  taylthlem1  24127  taylthlem2  24128  ulmshft  24144  mtestbdd  24159  iblulm  24161  itgulm2  24163  pserulm  24176  psercn2  24177  pserdvlem2  24182  pserdv  24183  pserdv2  24184  abelthlem1  24185  abelthlem3  24187  advlog  24400  advlogexp  24401  dvcxp1  24481  dvcxp2  24482  dvcncxp1  24484  sqrtcn  24491  loglesqrt  24499  dvatan  24662  atantayl2  24665  atantayl3  24666  leibpi  24669  rlimcnp2  24693  efrlim  24696  dfef2  24697  cxp2lim  24703  divsqrtsumlem  24706  lgamgulmlem2  24756  lgamgulm2  24762  lgamcvglem  24766  gamcvg2lem  24785  ftalem7  24805  basellem9  24815  muinv  24919  logfacrlim  24949  logexprlim  24950  dchrmulid2  24977  dchrinvcl  24978  lgseisenlem3  25102  lgseisenlem4  25103  chtppilimlem2  25163  chebbnd2  25166  chpchtlim  25168  chpo1ub  25169  rpvmasumlem  25176  dchrmusumlema  25182  dchrvmasumlem1  25184  dchrvmasumiflem2  25191  dchrisum0fno1  25200  rpvmasum2  25201  dchrisum0lema  25203  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0  25209  dchrmusumlem  25211  dchrvmasumlem  25212  rpvmasum  25215  rplogsum  25216  logdivsum  25222  mulog2sumlem3  25225  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  logsqvma2  25232  log2sumbnd  25233  selberglem2  25235  selberg3lem1  25246  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrsumo1  25254  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntrlog2bndlem2  25267  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  padicabvf  25320  padicabvcxp  25321  mirval  25550  crctcshlem4  26712  eucrct2eupth  27105  chscllem4  28499  brafnmul  28810  kbmul  28814  ofresid  29444  ofoprabco  29464  fcobijfs  29501  gsummpt2d  29781  gsummptres  29784  fzto1st1  29852  fzto1st  29853  mdetpmtr1  29889  mdetlap  29898  xrge0mulc1cn  29987  esumval  30108  esumsnf  30126  esumpcvgval  30140  esumcvg  30148  esumcvgsum  30150  esumsup  30151  ofcfeqd2  30163  meascnbl  30282  sitgval  30394  probmeasb  30492  cndprobprob  30500  dstfrvclim1  30539  ballotlemfval  30551  ballotlemsval  30570  ballotlemieq  30578  plymul02  30623  plymulx0  30624  plymulx  30625  signsplypnf  30627  signstfv  30640  signstfvn  30646  signstfvp  30648  itgexpif  30684  logdivsqrle  30728  ptpconn  31215  cvmliftlem6  31272  cvmliftphtlem  31299  cvmlift3lem5  31305  elmrsubrn  31417  msubfval  31421  msubco  31428  divcnvlin  31618  knoppcnlem9  32491  knoppcnlem10  32492  knoppcnlem11  32493  bj-finsumval0  33147  curf  33387  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem3  33412  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  broucube  33443  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  mbfposadd  33457  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  itgaddnclem2  33469  itgaddnc  33470  iblsubnc  33471  itgsubnc  33472  itgmulc2nclem1  33476  itgmulc2nclem2  33477  itgmulc2nc  33478  itgabsnc  33479  ftc1cnnclem  33483  ftc1anclem3  33487  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem8  33492  ftc1anc  33493  ftc2nc  33494  areacirclem1  33500  areacirclem2  33501  areacirclem4  33503  areacirc  33505  upixp  33524  mzpsubst  37311  mzprename  37312  mzpcompact2lem  37314  eldioph2  37325  rabdiophlem2  37366  mendlmod  37763  mendassa  37764  areaquad  37802  fsovcnvlem  38307  hashnzfzclim  38521  expgrowthi  38532  expgrowth  38534  uzmptshftfval  38545  dvradcnv2  38546  binomcxplemrat  38549  binomcxplemfrat  38550  binomcxplemradcnv  38551  binomcxplemdvbinom  38552  binomcxplemcvg  38553  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  mulc1cncfg  39821  expcnfg  39823  fprodcnlem  39831  clim1fr1  39833  divcnvg  39859  sublimc  39884  reclimc  39885  divlimc  39888  limsupresico  39932  limsuppnfdlem  39933  limsupvaluz  39940  supcnvlimsupmpt  39973  liminfresico  40003  climliminflimsupd  40033  cncfmptssg  40083  negcncfg  40094  cncficcgt0  40101  fprodcncf  40114  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  dvsinax  40127  dvasinbx  40135  dvdivf  40137  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmptdivc  40153  dvxpaek  40155  dvnxpaek  40157  dvnmul  40158  dvnprodlem2  40162  ibliccsinexp  40166  itgsinexplem1  40169  itgsinexp  40170  iblempty  40181  itgcoscmulx  40185  itgsincmulx  40190  itgioocnicc  40193  iblcncfioo  40194  itgsbtaddcnst  40198  volioofmpt  40211  volicofmpt  40214  stoweidlem4  40221  stirlinglem5  40295  dirkerval  40308  dirkertrigeq  40318  dirkeritg  40319  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem16  40340  fourierdlem18  40342  fourierdlem21  40345  fourierdlem22  40346  fourierdlem28  40352  fourierdlem39  40363  fourierdlem40  40364  fourierdlem41  40365  fourierdlem53  40376  fourierdlem56  40379  fourierdlem57  40380  fourierdlem60  40383  fourierdlem61  40384  fourierdlem68  40391  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem81  40404  fourierdlem82  40405  fourierdlem83  40406  fourierdlem84  40407  fourierdlem85  40408  fourierdlem88  40411  fourierdlem90  40413  fourierdlem92  40415  fourierdlem93  40416  fourierdlem95  40418  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  elaa2lem  40450  etransclem4  40455  etransclem17  40468  etransclem18  40469  etransclem32  40483  etransclem46  40497  sge0z  40592  sge0revalmpt  40595  sge0tsms  40597  sge0sup  40608  sge0iunmptlemre  40632  sge0iun  40636  sge0xaddlem2  40651  ismeannd  40684  psmeasurelem  40687  meaiuninclem  40697  meaiininclem  40700  caratheodory  40742  isomenndlem  40744  ovnval  40755  hoicvrrex  40770  ovnlecvr  40772  ovncvrrp  40778  ovn0lem  40779  ovnsubaddlem1  40784  hoidmv1lelem2  40806  hoidmv1le  40808  hoidmvlelem3  40811  ovnhoilem2  40816  ovnhoi  40817  ovnlecvr2  40824  ovncvr2  40825  hspmbllem2  40841  ovolval2lem  40857  ovolval3  40861  ovolval5lem1  40866  ovolval5lem2  40867  ovnovollem1  40870  ovnovollem2  40871  vonioolem1  40894  vonicclem1  40897  vonct  40907  smflim  40985  smfinflem  41023  smflimsuplem5  41030  smfliminflem  41036  fdmdifeqresdif  42120  ply1mulgsumlem2  42175  lincvalsc0  42210  linc0scn0  42212  lincdifsn  42213  lincsum  42218  lincscm  42219  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  lincresunit3lem2  42269  aacllem  42547  amgmwlem  42548