Theorem mpteq2dva 4502

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

Hypothesis

Ref	Expression
mpteq2dva.1	|- ( ( ph /\ x e. A ) -> B = C )

Assertion

Ref	Expression
mpteq2dva	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)

Proof of Theorem mpteq2dva

Step	Hyp	Ref	Expression
1		nfv 1771	. 2 |- F/ x ph
2		mpteq2dva.1	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	1, 2	mpteq2da 4501	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1454   e. wcel 1897   |-> cmpt 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-ral 2753  df-opab 4475  df-mpt 4476

This theorem is referenced by:  mpteq2dv  4503  2fvcoidd  6219  offval  6564  offval2  6574  caofinvl  6584  caofcom  6589  caofass  6591  caofdi  6593  caofdir  6594  caonncan  6595  curry1  6914  curry2  6917  mpt2curryd  7041  pw2f1olem  7701  mapxpen  7763  xpmapenlem  7764  cantnfp1  8211  cantnflem1d  8218  cantnflem1  8219  cnfcom2lem  8231  dfac12lem1  8598  seqof  12301  seqof2  12302  swrd0val  12813  swrdswrd  12852  repswswrd  12923  repswrevw  12925  revco  12967  ccatco  12968  repsco  12972  lo1eq  13680  rlimeq  13681  lo1mul2  13740  o1dif  13741  lo1sub  13742  rlimdiv  13757  caucvgr  13789  sumeq1  13803  fsumrlim  13919  fsumo1  13920  climfsum  13928  geomulcvg  13980  vdwlem8  14986  prmgapprmo  15081  restid2  15377  pwsplusgval  15436  pwsmulrval  15437  pwsvscafval  15440  qusin  15498  xpsaddlem  15529  xpsvsca  15533  catidd  15634  fuclid  15919  fucrid  15920  fucass  15921  setcepi  16031  prf1st  16137  prf2nd  16138  1st2ndprf  16139  curfcl  16165  curfuncf  16171  diag2  16178  curf2ndf  16180  hof2val  16189  hofcllem  16191  hofcl  16192  yonedalem4a  16208  yonedalem4c  16210  yonedalem3b  16212  yonedainv  16214  yonffthlem  16215  prdsidlem  16616  prdsmndd  16617  pwsco2mhm  16666  frmdup3lem  16698  frmdup3  16699  grpinvpropd  16777  prdsinvlem  16842  pwsinvg  16846  pwssub  16847  galactghm  17092  cayleylem1  17101  pmtrprfval  17176  sylow1lem2  17299  sylow3lem1  17327  efginvrel1  17426  frgpup3lem  17475  frgpup3  17476  prdscmnd  17547  iscyggen  17563  gsumval3  17589  gsumcllem  17590  gsumzsplit  17608  gsumsub  17629  gsummptf1o  17643  gsum2d  17652  gsum2d2  17654  gsumxp  17656  prdsgsum  17658  telgsumfz  17668  telgsumfz0  17670  telgsum  17672  dprdfsub  17702  dprdfeq0  17703  dprddisj2  17720  dprd2d2  17725  dpjidcl  17739  ablfaclem2  17767  ablfac2  17770  srgbinomlem3  17823  srgbinomlem4  17824  srgbinomlem  17825  gsumdixp  17885  prdsmgp  17886  prdsringd  17888  prdslmodd  18240  asclpropd  18618  psrass1lem  18649  psrlinv  18669  psrass1  18677  psrdi  18678  psrdir  18679  psrass23l  18680  psrcom  18681  psrass23  18682  resspsrmul  18689  mplsubrglem  18711  mplmonmul  18736  mplcoe1  18737  mplcoe5  18740  mplcoe4  18774  evlslem3  18785  evlslem1  18786  psrplusgpropd  18877  psropprmul  18879  coe1mul2  18910  coe1tm  18914  coe1tmmul2  18917  coe1tmmul  18918  coe1pwmul  18920  cply1mul  18935  ply1coe  18937  ply1coeOLD  18938  eqcoe1ply1eq  18939  lply1binomsc  18949  evl1gsummon  19001  mulgrhm2  19118  frgpcyg  19192  evpmodpmf1o  19212  phlpropd  19270  frlmphl  19387  uvcresum  19399  frlmup1  19404  mamures  19463  grpvrinv  19469  mhmvlin  19470  mamuass  19475  mamudi  19476  mamudir  19477  mamuvs1  19478  mamuvs2  19479  mpt2matmul  19519  mamutpos  19531  madetsumid  19534  dmatmul  19570  scmatscm  19586  1mavmul  19621  mavmulass  19622  mvmumamul1  19627  mulmarep1gsum1  19646  mulmarep1gsum2  19647  mdetleib2  19661  mdetfval1  19663  mdet0pr  19665  mdetdiag  19672  mdetdiagid  19673  mdetrlin  19675  mdetrsca  19676  mdetralt  19681  mdetunilem9  19693  gsummatr01  19732  smadiadetlem1a  19736  smadiadetlem3  19741  smadiadetlem4  19742  cpmatmcllem  19790  mat2pmatmul  19803  decpmatmullem  19843  decpmatmul  19844  pmatcollpw1lem2  19847  pmatcollpw  19853  pmatcollpw3lem  19855  pmatcollpwscmat  19863  idpm2idmp  19873  mp2pm2mplem3  19880  mp2pm2mplem4  19881  mp2pm2mplem5  19882  mp2pm2mp  19883  pm2mpghm  19888  pm2mpmhmlem2  19891  monmat2matmon  19896  pm2mp  19897  chpdmat  19913  chpscmat  19914  chpscmatgsumbin  19916  chpscmatgsummon  19917  chp0mat  19918  chpidmat  19919  chfacfscmulgsum  19932  chfacfpmmulgsum  19936  chfacfpmmulgsum2  19937  cayhamlem1  19938  cpmidgsumm2pm  19941  cpmidpmat  19945  cpmadugsumlemB  19946  cpmadugsumlemC  19947  cpmadugsumlemF  19948  cpmadumatpoly  19955  cayhamlem3  19959  cayhamlem4  19960  cayleyhamilton0  19961  cayleyhamiltonALT  19963  neiptopnei  20196  neiptopreu  20197  ptcnplem  20684  cnmpt1t  20728  cnmpt12  20730  cnmptkp  20743  cnmptk1  20744  cnmpt1k  20745  cnmptkk  20746  cnmptk1p  20748  cnmpt2k  20751  qtopeu  20779  pt1hmeo  20869  ptunhmeo  20871  xkocnv  20877  xkohmeo  20878  flfcnp2  21070  cnmpt1plusg  21150  istgp2  21154  tmdmulg  21155  tgpmulg  21156  tmdgsum  21158  symgtgp  21164  subgtgp  21168  tgpconcomp  21175  prdstgpd  21187  tsmsmhm  21208  tsmsadd  21209  tsmssub  21211  tgptsmscls  21212  tsmssplit  21214  tsmsxplem1  21215  tsmsxplem2  21216  cnmpt1vsca  21256  tlmtgp  21258  ustuqtoplem  21302  utopsnneip  21311  ressprdsds  21434  metuval  21612  nmfval2  21653  tngnm  21707  nmoeq0  21805  idnghm  21812  cnmpt1ds  21908  fsumcn  21950  expcn  21952  divccn  21953  divccncf  21986  negcncf  21998  copco  22097  pcopt  22101  pcopt2  22102  pcoass  22103  pi1xfrcnvlem  22135  cnmpt1ip  22266  rrxnm  22398  rrxds  22400  minveclem3b  22418  minveclem3bOLD  22430  ovolctb  22491  ovoliunnul  22508  voliunlem3  22553  ovolfs2  22571  uniioombllem2  22588  uniioombllem2OLD  22589  vitalilem4  22617  vitalilem5  22618  ismbf  22634  mbfss  22650  mbfmulc2re  22652  mbfneg  22654  mbfpos  22655  mbfposb  22657  mbfadd  22665  mbfsub  22666  mbfmulc2  22667  mbfinf  22669  mbfinfOLD  22670  mbflimsup  22671  mbflimsupOLD  22672  mbflimlem  22673  i1fpos  22712  i1fposd  22713  itg1climres  22720  mbfmul  22732  itg2mulc  22753  itg2i1fseq  22761  itg2cnlem1  22767  itg2cnlem2  22768  itgresr  22784  iblneg  22808  i1fibl  22813  itgitg1  22814  iblsub  22827  itgfsum  22832  itgmulc2lem1  22837  limcmpt  22886  limccnp  22894  limcco  22896  dvreslem  22912  dvres2lem  22913  dvidlem  22918  dvcnp2  22922  dvaddbr  22940  dvmulbr  22941  dvmulf  22945  dvcmulf  22947  dvcobr  22948  dvcof  22950  dvcjbr  22951  dvcj  22952  dvfre  22953  dvexp  22955  dvexp2  22956  dvrec  22957  dvmptcmul  22966  dvmptdivc  22967  dvmptneg  22968  dvmptsub  22969  dvmptre  22971  dvmptim  22972  dvmptfsum  22975  dvcnvlem  22976  dvcnv  22977  dvexp3  22978  dvef  22980  dvsincos  22981  dv11cn  23001  lhop2  23015  lhop  23016  ftc2  23044  itgparts  23047  itgsubstlem  23048  mdegfval  23059  mdegmullem  23075  ply1termlem  23205  plypow  23207  plyconst  23208  plyeq0lem  23212  plypf1  23214  plyaddlem1  23215  plymullem1  23216  coeeulem  23226  coeidlem  23239  plyco  23243  coeeq2  23244  0dgr  23247  0dgrb  23248  dgrcolem1  23275  dgrcolem2  23276  plycjlem  23278  dvply1  23285  dvply2g  23286  plydiveu  23299  plyremlem  23305  elqaalem3  23322  elqaalem3OLD  23325  taylfval  23362  dvtaylp  23373  taylthlem1  23376  taylthlem2  23377  ulmshft  23393  mtestbdd  23408  iblulm  23410  itgulm2  23412  pserulm  23425  psercn2  23426  pserdvlem2  23431  pserdv  23432  pserdv2  23433  abelthlem1  23434  abelthlem3  23436  advlog  23647  advlogexp  23648  dvcxp1  23728  dvcxp2  23729  dvcncxp1  23731  sqrtcn  23738  loglesqrt  23746  dvatan  23909  atantayl2  23912  atantayl3  23913  leibpi  23916  rlimcnp2  23940  efrlim  23943  dfef2  23944  cxp2lim  23950  divsqrtsumlem  23953  lgamgulmlem2  24003  lgamgulm2  24009  lgamcvglem  24013  gamcvg2lem  24032  ftalem7  24053  basellem9  24063  muinv  24170  logfacrlim  24200  logexprlim  24201  dchrmulid2  24228  dchrinvcl  24229  lgseisenlem3  24327  lgseisenlem4  24328  chtppilimlem2  24360  chebbnd2  24363  chpchtlim  24365  chpo1ub  24366  rpvmasumlem  24373  dchrmusumlema  24379  dchrvmasumlem1  24381  dchrvmasumiflem2  24388  dchrisum0fno1  24397  rpvmasum2  24398  dchrisum0lema  24400  dchrisum0lem1  24402  dchrisum0lem2a  24403  dchrisum0lem2  24404  dchrisum0  24406  dchrmusumlem  24408  dchrvmasumlem  24409  rpvmasum  24412  rplogsum  24413  logdivsum  24419  mulog2sumlem3  24422  vmalogdivsum2  24424  vmalogdivsum  24425  2vmadivsumlem  24426  logsqvma2  24429  log2sumbnd  24430  selberglem2  24432  selberg3lem1  24443  selberg3  24445  selberg4lem1  24446  selberg4  24447  pntrsumo1  24451  selberg3r  24455  selberg4r  24456  selberg34r  24457  pntrlog2bndlem2  24464  pntrlog2bndlem4  24466  pntrlog2bndlem5  24467  pntrlog2bndlem6  24469  padicabvf  24517  padicabvcxp  24518  mirval  24748  wwlknprop  25462  chscllem4  27341  brafnmul  27652  kbmul  27656  ofresid  28291  ofoprabco  28315  fcobijfs  28359  gsummpt2d  28592  gsummptres  28595  fzto1st1  28663  fzto1st  28664  mdetpmtr1  28697  mdetlap  28706  xrge0mulc1cn  28795  esumval  28915  esumsnf  28933  esumpcvgval  28947  esumcvg  28955  esumcvgsum  28957  esumsup  28958  ofcfeqd2  28970  meascnbl  29089  sitgval  29213  probmeasb  29311  cndprobprob  29319  dstfrvclim1  29358  ballotlemfval  29370  ballotlemsval  29389  ballotlemieq  29397  ballotlemsvalOLD  29427  ballotlemieqOLD  29435  ofccat  29477  plymul02  29483  plymulx0  29484  plymulx  29485  signsplypnf  29487  signstfv  29500  signstfvn  29506  signstfvp  29508  ptpcon  30004  cvmliftlem6  30061  cvmliftphtlem  30088  cvmlift3lem5  30094  elmrsubrn  30206  msubfval  30210  msubco  30217  divcnvlin  30415  bj-finsumval0  31746  poimirlem3  31987  poimirlem15  31999  poimirlem16  32000  poimirlem17  32001  poimirlem19  32003  poimirlem20  32004  broucube  32018  ovoliunnfl  32026  voliunnfl  32028  volsupnfl  32029  mbfposadd  32032  itg2addnclem  32037  itg2addnclem3  32039  itg2addnc  32040  itgaddnclem2  32045  itgaddnc  32046  iblsubnc  32047  itgsubnc  32048  itgmulc2nclem1  32052  itgmulc2nclem2  32053  itgmulc2nc  32054  itgabsnc  32055  ftc1cnnclem  32059  ftc1anclem3  32063  ftc1anclem5  32065  ftc1anclem6  32066  ftc1anclem8  32068  ftc1anc  32069  ftc2nc  32070  areacirclem1  32076  areacirclem2  32077  areacirclem4  32079  areacirc  32081  upixp  32100  mzpsubst  35634  mzprename  35635  mzpcompact2lem  35637  eldioph2  35648  rabdiophlem2  35689  mendlmod  36103  mendassa  36104  areaquad  36145  hashnzfzclim  36714  expgrowthi  36725  expgrowth  36727  uzmptshftfval  36738  dvradcnv2  36739  binomcxplemrat  36742  binomcxplemfrat  36743  binomcxplemradcnv  36744  binomcxplemdvbinom  36745  binomcxplemcvg  36746  binomcxplemdvsum  36747  binomcxplemnotnn0  36748  mulc1cncfg  37704  expcnfg  37708  clim1fr1  37716  divcnvg  37744  sublimc  37770  reclimc  37771  divlimc  37774  cncfmptssg  37784  negcncfg  37795  divcncf  37798  cncficcgt0  37803  fprodcncf  37816  dvrecg  37819  dvsinax  37820  dvmptdiv  37826  dvasinbx  37829  dvdivf  37831  ioodvbdlimc1lem2  37841  ioodvbdlimc1lem2OLD  37843  ioodvbdlimc2lem  37845  ioodvbdlimc2lemOLD  37846  dvnmptdivc  37850  dvxpaek  37852  dvnxpaek  37854  dvnmul  37855  dvnprodlem2  37859  ibliccsinexp  37864  itgsinexplem1  37867  itgsinexp  37868  iblempty  37879  itgcoscmulx  37883  itgsincmulx  37888  itgioocnicc  37891  iblcncfioo  37892  itgsbtaddcnst  37896  stoweidlem4  37901  stirlinglem5  37977  dirkerval  37990  dirkertrigeq  38000  dirkeritg  38001  dirkercncflem2  38003  dirkercncflem4  38005  fourierdlem16  38022  fourierdlem18  38024  fourierdlem21  38027  fourierdlem22  38028  fourierdlem28  38034  fourierdlem39  38046  fourierdlem40  38047  fourierdlem41  38048  fourierdlem53  38060  fourierdlem56  38063  fourierdlem57  38064  fourierdlem60  38067  fourierdlem61  38068  fourierdlem68  38075  fourierdlem73  38080  fourierdlem74  38081  fourierdlem75  38082  fourierdlem76  38083  fourierdlem78  38085  fourierdlem81  38088  fourierdlem82  38089  fourierdlem83  38090  fourierdlem84  38091  fourierdlem85  38092  fourierdlem88  38095  fourierdlem90  38097  fourierdlem92  38099  fourierdlem93  38100  fourierdlem95  38102  fourierdlem97  38104  fourierdlem101  38108  fourierdlem103  38110  fourierdlem104  38111  fourierdlem111  38118  fourierdlem112  38119  sqwvfoura  38129  sqwvfourb  38130  fouriersw  38132  elaa2lem  38134  elaa2lemOLD  38135  etransclem4  38140  etransclem17  38153  etransclem18  38154  etransclem32  38168  etransclem46  38182  sge0z  38254  sge0revalmpt  38257  sge0tsms  38259  sge0sup  38270  sge0iunmptlemre  38294  sge0iun  38298  sge0xaddlem2  38313  ismeannd  38342  psmeasurelem  38345  caratheodory  38386  isomenndlem  38388  ovnval  38399  hoicvrrex  38415  ovnlecvr  38417  ovncvrrp  38423  ovn0lem  38424  ovnsubaddlem1  38429  hoidmv1lelem2  38451  hoidmv1le  38453  hoidmvlelem3  38456  ovnhoilem2  38461  ovnhoi  38462  ovnlecvr2  38469  ovncvr2  38470  hspmbllem2  38486  fdmdifeqresdif  40395  ply1mulgsumlem2  40451  lincvalsc0  40486  linc0scn0  40488  lincdifsn  40489  lincsum  40494  lincscm  40495  lindslinindimp2lem4  40526  lindslinindsimp2lem5  40527  lincresunit3lem2  40545  aacllem  40812