Theorem mpteq2dva 5161

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 1915	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq2da 5160	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ↦ cmpt 5146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-opab 5129  df-mpt 5147

This theorem is referenced by:  mpteq2dv  5162  2fvcoidd  7053  offval  7416  offval2  7426  caofinvl  7436  caofcom  7441  caofass  7443  caofdi  7445  caofdir  7446  caonncan  7447  curry1  7799  curry2  7802  mpocurryd  7935  pw2f1olem  8621  mapxpen  8683  xpmapenlem  8684  cantnfp1  9144  cantnflem1d  9151  cantnflem1  9152  cnfcom2lem  9164  dfac12lem1  9569  seqof  13428  seqof2  13429  swrdswrd  14067  repswswrd  14146  repswrevw  14149  revco  14196  ccatco  14197  repsco  14202  ofccat  14329  lo1eq  14925  rlimeq  14926  lo1mul2  14985  o1dif  14986  lo1sub  14987  rlimdiv  15002  caucvgr  15032  sumeq1  15045  fsumrlim  15166  fsumo1  15167  climfsum  15175  geomulcvg  15232  vdwlem8  16324  prmgapprmo  16398  restid2  16704  pwsplusgval  16763  pwsmulrval  16764  pwsvscafval  16767  qusin  16817  xpsaddlem  16846  xpsvsca  16850  catidd  16951  fuclid  17236  fucrid  17237  fucass  17238  setcepi  17348  prf1st  17454  prf2nd  17455  1st2ndprf  17456  curfcl  17482  curfuncf  17488  diag2  17495  curf2ndf  17497  hof2val  17506  hofcllem  17508  hofcl  17509  yonedalem4a  17525  yonedalem4c  17527  yonedalem3b  17529  yonedainv  17531  yonffthlem  17532  prdsidlem  17943  prdsmndd  17944  pwsco2mhm  17997  frmdup3lem  18031  frmdup3  18032  smndex1gid  18068  smndex1igid  18069  grpinvpropd  18174  prdsinvlem  18208  pwsinvg  18212  pwssub  18213  galactghm  18532  cayleylem1  18540  pmtrprfval  18615  sylow1lem2  18724  sylow3lem1  18752  efginvrel1  18854  frgpup3lem  18903  frgpup3  18904  prdscmnd  18981  iscyggen  18999  gsumval3  19027  gsumcllem  19028  gsumzsplit  19047  gsumsub  19068  gsummptf1o  19083  gsum2d  19092  gsum2d2  19094  gsumxp  19096  prdsgsum  19101  telgsumfz  19110  telgsumfz0  19112  telgsum  19114  dprdfsub  19143  dprdfeq0  19144  dprddisj2  19161  dprd2d2  19166  dpjidcl  19180  ablfaclem2  19208  ablfac2  19211  srgbinomlem3  19292  srgbinomlem4  19293  srgbinomlem  19294  gsumdixp  19359  prdsmgp  19360  prdsringd  19362  prdslmodd  19741  asclpropd  20126  psrass1lem  20157  psrlinv  20177  psrass1  20185  psrdi  20186  psrdir  20187  psrass23l  20188  psrcom  20189  psrass23  20190  resspsrmul  20197  mplsubrglem  20219  mplmonmul  20245  mplcoe1  20246  mplcoe5  20249  mplcoe4  20283  evlslem3  20293  evlslem1  20295  psrplusgpropd  20404  psropprmul  20406  coe1mul2  20437  coe1tm  20441  coe1tmmul2  20444  coe1tmmul  20445  coe1pwmul  20447  cply1mul  20462  ply1coe  20464  eqcoe1ply1eq  20465  lply1binomsc  20475  evl1gsummon  20528  mulgrhm2  20646  frgpcyg  20720  evpmodpmf1o  20740  phlpropd  20799  frlmphl  20925  uvcresum  20937  frlmup1  20942  mamures  21001  grpvrinv  21007  mhmvlin  21008  mamuass  21011  mamudi  21012  mamudir  21013  mamuvs1  21014  mamuvs2  21015  mpomatmul  21055  mamutpos  21067  madetsumid  21070  dmatmul  21106  scmatscm  21122  1mavmul  21157  mavmulass  21158  mvmumamul1  21163  mulmarep1gsum1  21182  mulmarep1gsum2  21183  mdetleib2  21197  mdetfval1  21199  mdet0pr  21201  mdetdiag  21208  mdetdiagid  21209  mdetrlin  21211  mdetrsca  21212  mdetralt  21217  mdetunilem9  21229  gsummatr01  21268  smadiadetlem1a  21272  smadiadetlem3  21277  smadiadetlem4  21278  cpmatmcllem  21326  mat2pmatmul  21339  decpmatmullem  21379  decpmatmul  21380  pmatcollpw1lem2  21383  pmatcollpw  21389  pmatcollpw3lem  21391  pmatcollpwscmat  21399  idpm2idmp  21409  mp2pm2mplem3  21416  mp2pm2mplem4  21417  mp2pm2mplem5  21418  mp2pm2mp  21419  pm2mpghm  21424  pm2mpmhmlem2  21427  monmat2matmon  21432  pm2mp  21433  chpdmat  21449  chpscmat  21450  chpscmatgsumbin  21452  chpscmatgsummon  21453  chp0mat  21454  chpidmat  21455  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmidgsumm2pm  21477  cpmidpmat  21481  cpmadugsumlemB  21482  cpmadugsumlemC  21483  cpmadugsumlemF  21484  cpmadumatpoly  21491  cayhamlem3  21495  cayhamlem4  21496  cayleyhamilton0  21497  cayleyhamiltonALT  21499  neiptopnei  21740  neiptopreu  21741  ptcnplem  22229  cnmpt1t  22273  cnmpt12  22275  cnmptkp  22288  cnmptk1  22289  cnmpt1k  22290  cnmptkk  22291  cnmptk1p  22293  cnmpt2k  22296  qtopeu  22324  pt1hmeo  22414  ptunhmeo  22416  xkocnv  22422  xkohmeo  22423  flfcnp2  22615  cnmpt1plusg  22695  istgp2  22699  tmdmulg  22700  tgpmulg  22701  tmdgsum  22703  subgtgp  22713  symgtgp  22714  tgpconncomp  22721  prdstgpd  22733  tsmsmhm  22754  tsmsadd  22755  tsmssub  22757  tgptsmscls  22758  tsmssplit  22760  tsmsxplem1  22761  tsmsxplem2  22762  cnmpt1vsca  22802  tlmtgp  22804  ustuqtoplem  22848  utopsnneip  22857  ressprdsds  22981  metuval  23159  nmfval2  23200  tngnm  23260  nmoeq0  23345  idnghm  23352  cnmpt1ds  23450  fsumcn  23478  expcn  23480  divccn  23481  divccncf  23514  negcncf  23526  copco  23622  pcopt  23626  pcopt2  23627  pcoass  23628  pi1xfrcnvlem  23660  cnmpt1ip  23850  rrxnm  23994  rrxds  23996  minveclem3b  24031  divcncf  24048  ovolctb  24091  ovoliunnul  24108  voliunlem3  24153  ovolfs2  24172  uniioombllem2  24184  vitalilem4  24212  vitalilem5  24213  ismbf  24229  mbfss  24247  mbfmulc2re  24249  mbfneg  24251  mbfpos  24252  mbfposb  24254  mbfadd  24262  mbfsub  24263  mbfmulc2  24264  mbfinf  24266  mbflimsup  24267  mbflimlem  24268  i1fpos  24307  i1fposd  24308  itg1climres  24315  mbfmul  24327  itg2mulc  24348  itg2i1fseq  24356  itg2cnlem1  24362  itg2cnlem2  24363  itgresr  24379  iblneg  24403  i1fibl  24408  itgitg1  24409  iblsub  24422  itgfsum  24427  itgmulc2lem1  24432  limcmpt  24481  limccnp  24489  limcco  24491  dvreslem  24507  dvres2lem  24508  dvidlem  24513  dvcnp2  24517  dvaddbr  24535  dvmulbr  24536  dvmulf  24540  dvcmulf  24542  dvcobr  24543  dvcof  24545  dvcjbr  24546  dvcj  24547  dvfre  24548  dvexp  24550  dvexp2  24551  dvrec  24552  dvmptcmul  24561  dvmptdivc  24562  dvmptneg  24563  dvmptsub  24564  dvmptre  24566  dvmptim  24567  dvrecg  24570  dvmptdiv  24571  dvmptfsum  24572  dvcnvlem  24573  dvcnv  24574  dvexp3  24575  dvef  24577  dvsincos  24578  dv11cn  24598  lhop2  24612  lhop  24613  ftc2  24641  itgparts  24644  itgsubstlem  24645  mdegfval  24656  mdegmullem  24672  ply1termlem  24793  plypow  24795  plyconst  24796  plyeq0lem  24800  plypf1  24802  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  coeidlem  24827  plyco  24831  coeeq2  24832  0dgr  24835  0dgrb  24836  dgrcolem1  24863  dgrcolem2  24864  plycjlem  24866  dvply1  24873  dvply2g  24874  plydiveu  24887  plyremlem  24893  elqaalem3  24910  taylfval  24947  dvtaylp  24958  taylthlem1  24961  taylthlem2  24962  ulmshft  24978  mtestbdd  24993  iblulm  24995  itgulm2  24997  pserulm  25010  psercn2  25011  pserdvlem2  25016  pserdv  25017  pserdv2  25018  abelthlem1  25019  abelthlem3  25021  advlog  25237  advlogexp  25238  dvcxp1  25321  dvcxp2  25322  dvcncxp1  25324  sqrtcn  25331  loglesqrt  25339  dvatan  25513  atantayl2  25516  atantayl3  25517  leibpi  25520  rlimcnp2  25544  efrlim  25547  dfef2  25548  cxp2lim  25554  divsqrtsumlem  25557  lgamgulmlem2  25607  lgamgulm2  25613  lgamcvglem  25617  gamcvg2lem  25636  ftalem7  25656  basellem9  25666  muinv  25770  logfacrlim  25800  logexprlim  25801  dchrmulid2  25828  dchrinvcl  25829  lgseisenlem3  25953  lgseisenlem4  25954  chtppilimlem2  26050  chebbnd2  26053  chpchtlim  26055  chpo1ub  26056  rpvmasumlem  26063  dchrmusumlema  26069  dchrvmasumlem1  26071  dchrvmasumiflem2  26078  dchrisum0fno1  26087  rpvmasum2  26088  dchrisum0lema  26090  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrisum0  26096  dchrmusumlem  26098  dchrvmasumlem  26099  rpvmasum  26102  rplogsum  26103  logdivsum  26109  mulog2sumlem3  26112  vmalogdivsum2  26114  vmalogdivsum  26115  2vmadivsumlem  26116  logsqvma2  26119  log2sumbnd  26120  selberglem2  26122  selberg3lem1  26133  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrsumo1  26141  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntrlog2bndlem2  26154  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  padicabvf  26207  padicabvcxp  26208  mirval  26441  crctcshlem4  27598  clwlknf1oclwwlkn  27863  eucrct2eupth  28024  chscllem4  29417  brafnmul  29728  kbmul  29732  cofmpt2  30379  ofresid  30389  ofoprabco  30409  fcobijfs  30459  gsummpt2d  30687  gsummptres  30690  fzto1st1  30744  fzto1st  30745  freshmansdream  30859  lbsdiflsp0  31022  fedgmullem1  31025  fedgmullem2  31026  mdetpmtr1  31088  mdetlap  31097  xrge0mulc1cn  31184  esumval  31305  esumsnf  31323  esumpcvgval  31337  esumcvg  31345  esumcvgsum  31347  esumsup  31348  ofcfeqd2  31360  meascnbl  31478  sitgval  31590  probmeasb  31688  cndprobprob  31696  dstfrvclim1  31735  ballotlemfval  31747  ballotlemsval  31766  ballotlemieq  31774  plymul02  31816  plymulx0  31817  plymulx  31818  signsplypnf  31820  signstfv  31833  signstfvn  31839  signstfvp  31841  itgexpif  31877  logdivsqrle  31921  ptpconn  32480  cvmliftlem6  32537  cvmliftphtlem  32564  cvmlift3lem5  32570  elmrsubrn  32767  msubfval  32771  msubco  32778  divcnvlin  32964  knoppcnlem9  33840  knoppcnlem10  33841  knoppcnlem11  33842  bj-finsumval0  34570  curf  34885  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem3  34910  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  broucube  34941  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  mbfposadd  34954  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  itgaddnclem2  34966  itgaddnc  34967  iblsubnc  34968  itgsubnc  34969  itgmulc2nclem1  34973  itgmulc2nclem2  34974  itgmulc2nc  34975  itgabsnc  34976  ftc1cnnclem  34980  ftc1anclem3  34984  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem8  34989  ftc1anc  34990  ftc2nc  34991  areacirclem1  34997  areacirclem2  34998  areacirclem4  35000  areacirc  35002  upixp  35019  qsalrel  39174  mzpsubst  39394  mzprename  39395  mzpcompact2lem  39397  eldioph2  39408  rabdiophlem2  39448  mendlmod  39842  mendassa  39843  areaquad  39872  fsovcnvlem  40408  hashnzfzclim  40703  expgrowthi  40714  expgrowth  40716  uzmptshftfval  40727  dvradcnv2  40728  binomcxplemrat  40731  binomcxplemfrat  40732  binomcxplemradcnv  40733  binomcxplemdvbinom  40734  binomcxplemcvg  40735  binomcxplemdvsum  40736  binomcxplemnotnn0  40737  mulc1cncfg  41919  expcnfg  41921  fprodcnlem  41929  clim1fr1  41931  divcnvg  41957  sublimc  41982  reclimc  41983  divlimc  41986  limsupresico  42030  limsuppnfdlem  42031  limsupvaluz  42038  supcnvlimsupmpt  42071  liminfresico  42101  climliminflimsupd  42131  cncfmptssg  42202  negcncfg  42213  cncficcgt0  42220  fprodcncf  42233  fprodsubrecnncnvlem  42240  fprodaddrecnncnvlem  42242  dvsinax  42246  dvasinbx  42254  dvdivf  42256  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnmptdivc  42272  dvxpaek  42274  dvnxpaek  42276  dvnmul  42277  dvnprodlem2  42281  ibliccsinexp  42285  itgsinexplem1  42288  itgsinexp  42289  iblempty  42299  itgcoscmulx  42303  itgsincmulx  42308  itgioocnicc  42311  iblcncfioo  42312  itgsbtaddcnst  42316  volioofmpt  42328  volicofmpt  42331  stoweidlem4  42338  stirlinglem5  42412  dirkerval  42425  dirkertrigeq  42435  dirkeritg  42436  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem16  42457  fourierdlem18  42459  fourierdlem21  42462  fourierdlem22  42463  fourierdlem28  42469  fourierdlem39  42480  fourierdlem40  42481  fourierdlem41  42482  fourierdlem53  42493  fourierdlem56  42496  fourierdlem57  42497  fourierdlem60  42500  fourierdlem61  42501  fourierdlem68  42508  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fourierdlem81  42521  fourierdlem82  42522  fourierdlem83  42523  fourierdlem84  42524  fourierdlem85  42525  fourierdlem88  42528  fourierdlem90  42530  fourierdlem92  42532  fourierdlem93  42533  fourierdlem95  42535  fourierdlem97  42537  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem112  42552  sqwvfoura  42562  sqwvfourb  42563  fouriersw  42565  elaa2lem  42567  etransclem4  42572  etransclem17  42585  etransclem18  42586  etransclem32  42600  etransclem46  42614  sge0z  42706  sge0revalmpt  42709  sge0tsms  42711  sge0sup  42722  sge0iunmptlemre  42746  sge0iun  42750  sge0xaddlem2  42765  ismeannd  42798  psmeasurelem  42801  meaiuninclem  42811  meaiininclem  42817  caratheodory  42859  isomenndlem  42861  ovnval  42872  hoicvrrex  42887  ovnlecvr  42889  ovncvrrp  42895  ovn0lem  42896  ovnsubaddlem1  42901  hoidmv1lelem2  42923  hoidmv1le  42925  hoidmvlelem3  42928  ovnhoilem2  42933  ovnhoi  42934  ovnlecvr2  42941  ovncvr2  42942  hspmbllem2  42958  ovolval2lem  42974  ovolval3  42978  ovolval5lem1  42983  ovolval5lem2  42984  ovnovollem1  42987  ovnovollem2  42988  vonioolem1  43011  vonicclem1  43014  vonct  43024  smflim  43102  smfinflem  43140  smflimsuplem5  43147  smfliminflem  43153  fundcmpsurbijinjpreimafv  43616  fundcmpsurinjimaid  43620  fdmdifeqresdif  44439  ply1mulgsumlem2  44490  lincvalsc0  44525  linc0scn0  44527  lincdifsn  44528  lincsum  44533  lincscm  44534  lindslinindimp2lem4  44565  lindslinindsimp2lem5  44566  lincresunit3lem2  44584  aacllem  44951  amgmwlem  44952