Theorem mpteq2dva 5125

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-opab 5093  df-mpt 5111

This theorem is referenced by:  mpteq2dv  5126  2fvcoidd  7031  offval  7396  offval2  7406  caofinvl  7416  caofcom  7421  caofass  7423  caofdi  7425  caofdir  7426  caonncan  7427  curry1  7782  curry2  7785  mpocurryd  7918  pw2f1olem  8604  mapxpen  8667  xpmapenlem  8668  cantnfp1  9128  cantnflem1d  9135  cantnflem1  9136  cnfcom2lem  9148  dfac12lem1  9554  seqof  13423  seqof2  13424  swrdswrd  14058  repswswrd  14137  repswrevw  14140  revco  14187  ccatco  14188  repsco  14193  ofccat  14320  lo1eq  14917  rlimeq  14918  lo1mul2  14977  o1dif  14978  lo1sub  14979  rlimdiv  14994  caucvgr  15024  sumeq1  15037  fsumrlim  15158  fsumo1  15159  climfsum  15167  geomulcvg  15224  vdwlem8  16314  prmgapprmo  16388  restid2  16696  pwsplusgval  16755  pwsmulrval  16756  pwsvscafval  16759  qusin  16809  xpsaddlem  16838  xpsvsca  16842  catidd  16943  fuclid  17228  fucrid  17229  fucass  17230  setcepi  17340  prf1st  17446  prf2nd  17447  1st2ndprf  17448  curfcl  17474  curfuncf  17480  diag2  17487  curf2ndf  17489  hof2val  17498  hofcllem  17500  hofcl  17501  yonedalem4a  17517  yonedalem4c  17519  yonedalem3b  17521  yonedainv  17523  yonffthlem  17524  prdsidlem  17935  prdsmndd  17936  pwsco2mhm  17989  frmdup3lem  18023  frmdup3  18024  smndex1gid  18060  smndex1igid  18061  grpinvpropd  18166  prdsinvlem  18200  pwsinvg  18204  pwssub  18205  galactghm  18524  cayleylem1  18532  pmtrprfval  18607  sylow1lem2  18716  sylow3lem1  18744  efginvrel1  18846  frgpup3lem  18895  frgpup3  18896  prdscmnd  18974  iscyggen  18992  gsumval3  19020  gsumcllem  19021  gsumzsplit  19040  gsumsub  19061  gsummptf1o  19076  gsum2d  19085  gsum2d2  19087  gsumxp  19089  prdsgsum  19094  telgsumfz  19103  telgsumfz0  19105  telgsum  19107  dprdfsub  19136  dprdfeq0  19137  dprddisj2  19154  dprd2d2  19159  dpjidcl  19173  ablfaclem2  19201  ablfac2  19204  srgbinomlem3  19285  srgbinomlem4  19286  srgbinomlem  19287  gsumdixp  19355  prdsmgp  19356  prdsringd  19358  prdslmodd  19734  mulgrhm2  20192  frgpcyg  20265  evpmodpmf1o  20285  phlpropd  20344  frlmphl  20470  uvcresum  20482  frlmup1  20487  asclpropd  20583  psrass1lem  20615  psrlinv  20635  psrass1  20643  psrdi  20644  psrdir  20645  psrass23l  20646  psrcom  20647  psrass23  20648  resspsrmul  20655  mplsubrglem  20677  mplmonmul  20704  mplcoe1  20705  mplcoe5  20708  mplcoe4  20742  evlslem3  20752  evlslem1  20754  psrplusgpropd  20865  psropprmul  20867  coe1mul2  20898  coe1tm  20902  coe1tmmul2  20905  coe1tmmul  20906  coe1pwmul  20908  cply1mul  20923  ply1coe  20925  eqcoe1ply1eq  20926  lply1binomsc  20936  evl1gsummon  20989  mamures  20997  grpvrinv  21003  mhmvlin  21004  mamuass  21007  mamudi  21008  mamudir  21009  mamuvs1  21010  mamuvs2  21011  mpomatmul  21051  mamutpos  21063  madetsumid  21066  dmatmul  21102  scmatscm  21118  1mavmul  21153  mavmulass  21154  mvmumamul1  21159  mulmarep1gsum1  21178  mulmarep1gsum2  21179  mdetleib2  21193  mdetfval1  21195  mdet0pr  21197  mdetdiag  21204  mdetdiagid  21205  mdetrlin  21207  mdetrsca  21208  mdetralt  21213  mdetunilem9  21225  gsummatr01  21264  smadiadetlem1a  21268  smadiadetlem3  21273  smadiadetlem4  21274  cpmatmcllem  21323  mat2pmatmul  21336  decpmatmullem  21376  decpmatmul  21377  pmatcollpw1lem2  21380  pmatcollpw  21386  pmatcollpw3lem  21388  pmatcollpwscmat  21396  idpm2idmp  21406  mp2pm2mplem3  21413  mp2pm2mplem4  21414  mp2pm2mplem5  21415  mp2pm2mp  21416  pm2mpghm  21421  pm2mpmhmlem2  21424  monmat2matmon  21429  pm2mp  21430  chpdmat  21446  chpscmat  21447  chpscmatgsumbin  21449  chpscmatgsummon  21450  chp0mat  21451  chpidmat  21452  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  chfacfpmmulgsum2  21470  cayhamlem1  21471  cpmidgsumm2pm  21474  cpmidpmat  21478  cpmadugsumlemB  21479  cpmadugsumlemC  21480  cpmadugsumlemF  21481  cpmadumatpoly  21488  cayhamlem3  21492  cayhamlem4  21493  cayleyhamilton0  21494  cayleyhamiltonALT  21496  neiptopnei  21737  neiptopreu  21738  ptcnplem  22226  cnmpt1t  22270  cnmpt12  22272  cnmptkp  22285  cnmptk1  22286  cnmpt1k  22287  cnmptkk  22288  cnmptk1p  22290  cnmpt2k  22293  qtopeu  22321  pt1hmeo  22411  ptunhmeo  22413  xkocnv  22419  xkohmeo  22420  flfcnp2  22612  cnmpt1plusg  22692  istgp2  22696  tmdmulg  22697  tgpmulg  22698  tmdgsum  22700  subgtgp  22710  symgtgp  22711  tgpconncomp  22718  prdstgpd  22730  tsmsmhm  22751  tsmsadd  22752  tsmssub  22754  tgptsmscls  22755  tsmssplit  22757  tsmsxplem1  22758  tsmsxplem2  22759  cnmpt1vsca  22799  tlmtgp  22801  ustuqtoplem  22845  utopsnneip  22854  ressprdsds  22978  metuval  23156  nmfval2  23197  tngnm  23257  nmoeq0  23342  idnghm  23349  cnmpt1ds  23447  fsumcn  23475  expcn  23477  divccn  23478  divccncf  23511  negcncf  23527  copco  23623  pcopt  23627  pcopt2  23628  pcoass  23629  pi1xfrcnvlem  23661  cnmpt1ip  23851  rrxnm  23995  rrxds  23997  minveclem3b  24032  divcncf  24051  ovolctb  24094  ovoliunnul  24111  voliunlem3  24156  ovolfs2  24175  uniioombllem2  24187  vitalilem4  24215  vitalilem5  24216  ismbf  24232  mbfss  24250  mbfmulc2re  24252  mbfneg  24254  mbfpos  24255  mbfposb  24257  mbfadd  24265  mbfsub  24266  mbfmulc2  24267  mbfinf  24269  mbflimsup  24270  mbflimlem  24271  i1fpos  24310  i1fposd  24311  itg1climres  24318  mbfmul  24330  itg2mulc  24351  itg2i1fseq  24359  itg2cnlem1  24365  itg2cnlem2  24366  itgresr  24382  iblneg  24406  i1fibl  24411  itgitg1  24412  iblsub  24425  itgfsum  24430  itgmulc2lem1  24435  limcmpt  24486  limccnp  24494  limcco  24496  dvreslem  24512  dvres2lem  24513  dvidlem  24518  dvcnp2  24523  dvaddbr  24541  dvmulbr  24542  dvmulf  24546  dvcmulf  24548  dvcobr  24549  dvcof  24551  dvcjbr  24552  dvcj  24553  dvfre  24554  dvexp  24556  dvexp2  24557  dvrec  24558  dvmptcmul  24567  dvmptdivc  24568  dvmptneg  24569  dvmptsub  24570  dvmptre  24572  dvmptim  24573  dvrecg  24576  dvmptdiv  24577  dvmptfsum  24578  dvcnvlem  24579  dvcnv  24580  dvexp3  24581  dvef  24583  dvsincos  24584  dv11cn  24604  lhop2  24618  lhop  24619  ftc2  24647  itgparts  24650  itgsubstlem  24651  mdegfval  24663  mdegmullem  24679  ply1termlem  24800  plypow  24802  plyconst  24803  plyeq0lem  24807  plypf1  24809  plyaddlem1  24810  plymullem1  24811  coeeulem  24821  coeidlem  24834  plyco  24838  coeeq2  24839  0dgr  24842  0dgrb  24843  dgrcolem1  24870  dgrcolem2  24871  plycjlem  24873  dvply1  24880  dvply2g  24881  plydiveu  24894  plyremlem  24900  elqaalem3  24917  taylfval  24954  dvtaylp  24965  taylthlem1  24968  taylthlem2  24969  ulmshft  24985  mtestbdd  25000  iblulm  25002  itgulm2  25004  pserulm  25017  psercn2  25018  pserdvlem2  25023  pserdv  25024  pserdv2  25025  abelthlem1  25026  abelthlem3  25028  advlog  25245  advlogexp  25246  dvcxp1  25329  dvcxp2  25330  dvcncxp1  25332  sqrtcn  25339  loglesqrt  25347  dvatan  25521  atantayl2  25524  atantayl3  25525  leibpi  25528  rlimcnp2  25552  efrlim  25555  dfef2  25556  cxp2lim  25562  divsqrtsumlem  25565  lgamgulmlem2  25615  lgamgulm2  25621  lgamcvglem  25625  gamcvg2lem  25644  ftalem7  25664  basellem9  25674  muinv  25778  logfacrlim  25808  logexprlim  25809  dchrmulid2  25836  dchrinvcl  25837  lgseisenlem3  25961  lgseisenlem4  25962  chtppilimlem2  26058  chebbnd2  26061  chpchtlim  26063  chpo1ub  26064  rpvmasumlem  26071  dchrmusumlema  26077  dchrvmasumlem1  26079  dchrvmasumiflem2  26086  dchrisum0fno1  26095  rpvmasum2  26096  dchrisum0lema  26098  dchrisum0lem1  26100  dchrisum0lem2a  26101  dchrisum0lem2  26102  dchrisum0  26104  dchrmusumlem  26106  dchrvmasumlem  26107  rpvmasum  26110  rplogsum  26111  logdivsum  26117  mulog2sumlem3  26120  vmalogdivsum2  26122  vmalogdivsum  26123  2vmadivsumlem  26124  logsqvma2  26127  log2sumbnd  26128  selberglem2  26130  selberg3lem1  26141  selberg3  26143  selberg4lem1  26144  selberg4  26145  pntrsumo1  26149  selberg3r  26153  selberg4r  26154  selberg34r  26155  pntrlog2bndlem2  26162  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  padicabvf  26215  padicabvcxp  26216  mirval  26449  crctcshlem4  27606  clwlknf1oclwwlkn  27869  eucrct2eupth  28030  chscllem4  29423  brafnmul  29734  kbmul  29738  cofmpt2  30393  ofresid  30403  ofoprabco  30427  fcobijfs  30485  gsummpt2d  30734  gsummptres  30737  gsummptres2  30738  gsumpart  30740  gsumhashmul  30741  fzto1st1  30794  fzto1st  30795  freshmansdream  30909  elrspunidl  31014  lbsdiflsp0  31110  fedgmullem1  31113  fedgmullem2  31114  mdetpmtr1  31176  mdetlap  31185  xrge0mulc1cn  31294  esumval  31415  esumsnf  31433  esumpcvgval  31447  esumcvg  31455  esumcvgsum  31457  esumsup  31458  ofcfeqd2  31470  meascnbl  31588  sitgval  31700  probmeasb  31798  cndprobprob  31806  dstfrvclim1  31845  ballotlemfval  31857  ballotlemsval  31876  ballotlemieq  31884  plymul02  31926  plymulx0  31927  plymulx  31928  signsplypnf  31930  signstfv  31943  signstfvn  31949  signstfvp  31951  itgexpif  31987  logdivsqrle  32031  ptpconn  32593  cvmliftlem6  32650  cvmliftphtlem  32677  cvmlift3lem5  32683  elmrsubrn  32880  msubfval  32884  msubco  32891  divcnvlin  33077  knoppcnlem9  33953  knoppcnlem10  33954  knoppcnlem11  33955  bj-finsumval0  34700  curf  35035  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem3  35060  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  broucube  35091  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  mbfposadd  35104  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  itgaddnclem2  35116  itgaddnc  35117  iblsubnc  35118  itgsubnc  35119  itgmulc2nclem1  35123  itgmulc2nclem2  35124  itgmulc2nc  35125  itgabsnc  35126  ftc1cnnclem  35128  ftc1anclem3  35132  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem8  35137  ftc1anc  35138  ftc2nc  35139  areacirclem1  35145  areacirclem2  35146  areacirclem4  35148  areacirc  35150  upixp  35167  lcmineqlem8  39324  lcmineqlem12  39328  qsalrel  39420  fsuppssindlem1  39457  fsuppssind  39459  mzpsubst  39689  mzprename  39690  mzpcompact2lem  39692  eldioph2  39703  rabdiophlem2  39743  mendlmod  40137  mendassa  40138  areaquad  40166  fsovcnvlem  40714  hashnzfzclim  41026  expgrowthi  41037  expgrowth  41039  uzmptshftfval  41050  dvradcnv2  41051  binomcxplemrat  41054  binomcxplemfrat  41055  binomcxplemradcnv  41056  binomcxplemdvbinom  41057  binomcxplemcvg  41058  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  mulc1cncfg  42231  expcnfg  42233  fprodcnlem  42241  clim1fr1  42243  divcnvg  42269  sublimc  42294  reclimc  42295  divlimc  42298  limsupresico  42342  limsuppnfdlem  42343  limsupvaluz  42350  supcnvlimsupmpt  42383  liminfresico  42413  climliminflimsupd  42443  cncfmptssg  42513  negcncfg  42523  cncficcgt0  42530  fprodcncf  42542  fprodsubrecnncnvlem  42549  fprodaddrecnncnvlem  42551  dvsinax  42555  dvasinbx  42562  dvdivf  42564  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnmptdivc  42580  dvxpaek  42582  dvnxpaek  42584  dvnmul  42585  dvnprodlem2  42589  ibliccsinexp  42593  itgsinexplem1  42596  itgsinexp  42597  iblempty  42607  itgcoscmulx  42611  itgsincmulx  42616  itgioocnicc  42619  iblcncfioo  42620  itgsbtaddcnst  42624  volioofmpt  42636  volicofmpt  42639  stoweidlem4  42646  stirlinglem5  42720  dirkerval  42733  dirkertrigeq  42743  dirkeritg  42744  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem16  42765  fourierdlem18  42767  fourierdlem21  42770  fourierdlem22  42771  fourierdlem28  42777  fourierdlem39  42788  fourierdlem40  42789  fourierdlem41  42790  fourierdlem53  42801  fourierdlem56  42804  fourierdlem57  42805  fourierdlem60  42808  fourierdlem61  42809  fourierdlem68  42816  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem78  42826  fourierdlem81  42829  fourierdlem82  42830  fourierdlem83  42831  fourierdlem84  42832  fourierdlem85  42833  fourierdlem88  42836  fourierdlem90  42838  fourierdlem92  42840  fourierdlem93  42841  fourierdlem95  42843  fourierdlem97  42845  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem112  42860  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  elaa2lem  42875  etransclem4  42880  etransclem17  42893  etransclem18  42894  etransclem32  42908  etransclem46  42922  sge0z  43014  sge0revalmpt  43017  sge0tsms  43019  sge0sup  43030  sge0iunmptlemre  43054  sge0iun  43058  sge0xaddlem2  43073  ismeannd  43106  psmeasurelem  43109  meaiuninclem  43119  meaiininclem  43125  caratheodory  43167  isomenndlem  43169  ovnval  43180  hoicvrrex  43195  ovnlecvr  43197  ovncvrrp  43203  ovn0lem  43204  ovnsubaddlem1  43209  hoidmv1lelem2  43231  hoidmv1le  43233  hoidmvlelem3  43236  ovnhoilem2  43241  ovnhoi  43242  ovnlecvr2  43249  ovncvr2  43250  hspmbllem2  43266  ovolval2lem  43282  ovolval3  43286  ovolval5lem1  43291  ovolval5lem2  43292  ovnovollem1  43295  ovnovollem2  43296  vonioolem1  43319  vonicclem1  43322  vonct  43332  smflim  43410  smfinflem  43448  smflimsuplem5  43455  smfliminflem  43461  fundcmpsurbijinjpreimafv  43924  fundcmpsurinjimaid  43928  fdmdifeqresdif  44743  ply1mulgsumlem2  44795  lincvalsc0  44830  linc0scn0  44832  lincdifsn  44833  lincsum  44838  lincscm  44839  lindslinindimp2lem4  44870  lindslinindsimp2lem5  44871  lincresunit3lem2  44889  1arymaptfo  45057  itcovalpclem1  45084  itcovalpclem2  45085  itcovalt2lem1  45089  itcovalt2lem2  45090  aacllem  45329  amgmwlem  45330