Theorem mpteq2dva 4512

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 1754	. 2 |- F/ x ph
2		mpteq2dva.1	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	1, 2	mpteq2da 4511	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1870   |-> cmpt 4484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-ral 2787  df-opab 4485  df-mpt 4486

This theorem is referenced by:  mpteq2dv  4513  2fvcoidd  6210  offval  6552  offval2  6562  caofinvl  6572  caofcom  6577  caofass  6579  caofdi  6581  caofdir  6582  caonncan  6583  curry1  6899  curry2  6902  mpt2curryd  7024  pw2f1olem  7682  mapxpen  7744  xpmapenlem  7745  cantnfp1  8185  cantnflem1d  8192  cantnflem1  8193  cnfcom2lem  8205  dfac12lem1  8571  seqof  12267  seqof2  12268  swrd0val  12762  swrdswrd  12801  repswswrd  12872  repswrevw  12874  revco  12916  ccatco  12917  repsco  12921  lo1eq  13610  rlimeq  13611  lo1mul2  13670  o1dif  13671  lo1sub  13672  rlimdiv  13687  caucvgr  13719  sumeq1  13733  fsumrlim  13849  fsumo1  13850  climfsum  13858  geomulcvg  13910  vdwlem8  14892  prmgapprmo  14987  restid2  15279  pwsplusgval  15338  pwsmulrval  15339  pwsvscafval  15342  qusin  15392  xpsaddlem  15423  xpsvsca  15427  catidd  15528  fuclid  15813  fucrid  15814  fucass  15815  setcepi  15925  prf1st  16031  prf2nd  16032  1st2ndprf  16033  curfcl  16059  curfuncf  16065  diag2  16072  curf2ndf  16074  hof2val  16083  hofcllem  16085  hofcl  16086  yonedalem4a  16102  yonedalem4c  16104  yonedalem3b  16106  yonedainv  16108  yonffthlem  16109  prdsidlem  16510  prdsmndd  16511  pwsco2mhm  16560  frmdup3lem  16592  frmdup3  16593  grpinvpropd  16671  prdsinvlem  16736  pwsinvg  16740  pwssub  16741  galactghm  16986  cayleylem1  16995  pmtrprfval  17070  sylow1lem2  17177  sylow3lem1  17205  efginvrel1  17304  frgpup3lem  17353  frgpup3  17354  prdscmnd  17425  iscyggen  17441  gsumval3  17467  gsumcllem  17468  gsumzsplit  17486  gsumsub  17507  gsummptf1o  17521  gsum2d  17530  gsum2d2  17532  gsumxp  17534  prdsgsum  17536  telgsumfz  17546  telgsumfz0  17548  telgsum  17550  dprdfsub  17580  dprdfeq0  17581  dprddisj2  17598  dprd2d2  17603  dpjidcl  17617  ablfaclem2  17645  ablfac2  17648  srgbinomlem3  17701  srgbinomlem4  17702  srgbinomlem  17703  gsumdixp  17763  prdsmgp  17764  prdsringd  17766  prdslmodd  18118  asclpropd  18496  psrass1lem  18527  psrlinv  18547  psrass1  18555  psrdi  18556  psrdir  18557  psrass23l  18558  psrcom  18559  psrass23  18560  resspsrmul  18567  mplsubrglem  18589  mplmonmul  18614  mplcoe1  18615  mplcoe5  18618  mplcoe4  18652  evlslem3  18663  evlslem1  18664  psrplusgpropd  18755  psropprmul  18757  coe1mul2  18788  coe1tm  18792  coe1tmmul2  18795  coe1tmmul  18796  coe1pwmul  18798  cply1mul  18813  ply1coe  18815  ply1coeOLD  18816  eqcoe1ply1eq  18817  lply1binomsc  18827  evl1gsummon  18879  mulgrhm2  18992  frgpcyg  19066  evpmodpmf1o  19086  phlpropd  19144  frlmphl  19261  uvcresum  19273  frlmup1  19278  mamures  19337  grpvrinv  19343  mhmvlin  19344  mamuass  19349  mamudi  19350  mamudir  19351  mamuvs1  19352  mamuvs2  19353  mpt2matmul  19393  mamutpos  19405  madetsumid  19408  dmatmul  19444  scmatscm  19460  1mavmul  19495  mavmulass  19496  mvmumamul1  19501  mulmarep1gsum1  19520  mulmarep1gsum2  19521  mdetleib2  19535  mdetfval1  19537  mdet0pr  19539  mdetdiag  19546  mdetdiagid  19547  mdetrlin  19549  mdetrsca  19550  mdetralt  19555  mdetunilem9  19567  gsummatr01  19606  smadiadetlem1a  19610  smadiadetlem3  19615  smadiadetlem4  19616  cpmatmcllem  19664  mat2pmatmul  19677  decpmatmullem  19717  decpmatmul  19718  pmatcollpw1lem2  19721  pmatcollpw  19727  pmatcollpw3lem  19729  pmatcollpwscmat  19737  idpm2idmp  19747  mp2pm2mplem3  19754  mp2pm2mplem4  19755  mp2pm2mplem5  19756  mp2pm2mp  19757  pm2mpghm  19762  pm2mpmhmlem2  19765  monmat2matmon  19770  pm2mp  19771  chpdmat  19787  chpscmat  19788  chpscmatgsumbin  19790  chpscmatgsummon  19791  chp0mat  19792  chpidmat  19793  chfacfscmulgsum  19806  chfacfpmmulgsum  19810  chfacfpmmulgsum2  19811  cayhamlem1  19812  cpmidgsumm2pm  19815  cpmidpmat  19819  cpmadugsumlemB  19820  cpmadugsumlemC  19821  cpmadugsumlemF  19822  cpmadumatpoly  19829  cayhamlem3  19833  cayhamlem4  19834  cayleyhamilton0  19835  cayleyhamiltonALT  19837  neiptopnei  20070  neiptopreu  20071  ptcnplem  20558  cnmpt1t  20602  cnmpt12  20604  cnmptkp  20617  cnmptk1  20618  cnmpt1k  20619  cnmptkk  20620  cnmptk1p  20622  cnmpt2k  20625  qtopeu  20653  pt1hmeo  20743  ptunhmeo  20745  xkocnv  20751  xkohmeo  20752  flfcnp2  20944  cnmpt1plusg  21024  istgp2  21028  tmdmulg  21029  tgpmulg  21030  tmdgsum  21032  symgtgp  21038  subgtgp  21042  tgpconcomp  21049  prdstgpd  21061  tsmsmhm  21082  tsmsadd  21083  tsmssub  21085  tgptsmscls  21086  tsmssplit  21088  tsmsxplem1  21089  tsmsxplem2  21090  cnmpt1vsca  21130  tlmtgp  21132  ustuqtoplem  21176  utopsnneip  21185  ressprdsds  21308  metuval  21486  nmfval2  21527  tngnm  21581  nmoeq0  21659  idnghm  21666  cnmpt1ds  21762  fsumcn  21789  expcn  21791  divccn  21792  divccncf  21825  negcncf  21837  copco  21933  pcopt  21937  pcopt2  21938  pcoass  21939  pi1xfrcnvlem  21971  cnmpt1ip  22102  rrxnm  22234  rrxds  22236  minveclem3b  22254  ovolctb  22312  ovoliunnul  22329  voliunlem3  22373  ovolfs2  22391  uniioombllem2  22408  uniioombllem2OLD  22409  vitalilem4  22437  vitalilem5  22438  ismbf  22454  mbfss  22470  mbfmulc2re  22472  mbfneg  22474  mbfpos  22475  mbfposb  22477  mbfadd  22485  mbfsub  22486  mbfmulc2  22487  mbfinf  22489  mbfinfOLD  22490  mbflimsup  22491  mbflimsupOLD  22492  mbflimlem  22493  i1fpos  22532  i1fposd  22533  itg1climres  22540  mbfmul  22552  itg2mulc  22573  itg2i1fseq  22581  itg2cnlem1  22587  itg2cnlem2  22588  itgresr  22604  iblneg  22628  i1fibl  22633  itgitg1  22634  iblsub  22647  itgfsum  22652  itgmulc2lem1  22657  limcmpt  22706  limccnp  22714  limcco  22716  dvreslem  22732  dvres2lem  22733  dvidlem  22738  dvcnp2  22742  dvaddbr  22760  dvmulbr  22761  dvmulf  22765  dvcmulf  22767  dvcobr  22768  dvcof  22770  dvcjbr  22771  dvcj  22772  dvfre  22773  dvexp  22775  dvexp2  22776  dvrec  22777  dvmptcmul  22786  dvmptdivc  22787  dvmptneg  22788  dvmptsub  22789  dvmptre  22791  dvmptim  22792  dvmptfsum  22795  dvcnvlem  22796  dvcnv  22797  dvexp3  22798  dvef  22800  dvsincos  22801  dv11cn  22821  lhop2  22835  lhop  22836  ftc2  22864  itgparts  22867  itgsubstlem  22868  mdegfval  22879  mdegmullem  22895  ply1termlem  23016  plypow  23018  plyconst  23019  plyeq0lem  23023  plypf1  23025  plyaddlem1  23026  plymullem1  23027  coeeulem  23037  coeidlem  23050  plyco  23054  coeeq2  23055  0dgr  23058  0dgrb  23059  dgrcolem1  23086  dgrcolem2  23087  plycjlem  23089  dvply1  23096  dvply2g  23097  plydiveu  23110  plyremlem  23116  elqaalem3  23133  taylfval  23170  dvtaylp  23181  taylthlem1  23184  taylthlem2  23185  ulmshft  23201  mtestbdd  23216  iblulm  23218  itgulm2  23220  pserulm  23233  psercn2  23234  pserdvlem2  23239  pserdv  23240  pserdv2  23241  abelthlem1  23242  abelthlem3  23244  advlog  23455  advlogexp  23456  dvcxp1  23536  dvcxp2  23537  dvcncxp1  23539  sqrtcn  23546  loglesqrt  23554  dvatan  23717  atantayl2  23720  atantayl3  23721  leibpi  23724  rlimcnp2  23748  efrlim  23751  dfef2  23752  cxp2lim  23758  divsqrtsumlem  23761  lgamgulmlem2  23811  lgamgulm2  23817  lgamcvglem  23821  gamcvg2lem  23840  ftalem7  23859  basellem9  23869  muinv  23976  logfacrlim  24006  logexprlim  24007  dchrmulid2  24034  dchrinvcl  24035  lgseisenlem3  24133  lgseisenlem4  24134  chtppilimlem2  24166  chebbnd2  24169  chpchtlim  24171  chpo1ub  24172  rpvmasumlem  24179  dchrmusumlema  24185  dchrvmasumlem1  24187  dchrvmasumiflem2  24194  dchrisum0fno1  24203  rpvmasum2  24204  dchrisum0lema  24206  dchrisum0lem1  24208  dchrisum0lem2a  24209  dchrisum0lem2  24210  dchrisum0  24212  dchrmusumlem  24214  dchrvmasumlem  24215  rpvmasum  24218  rplogsum  24219  logdivsum  24225  mulog2sumlem3  24228  vmalogdivsum2  24230  vmalogdivsum  24231  2vmadivsumlem  24232  logsqvma2  24235  log2sumbnd  24236  selberglem2  24238  selberg3lem1  24249  selberg3  24251  selberg4lem1  24252  selberg4  24253  pntrsumo1  24257  selberg3r  24261  selberg4r  24262  selberg34r  24263  pntrlog2bndlem2  24270  pntrlog2bndlem4  24272  pntrlog2bndlem5  24273  pntrlog2bndlem6  24275  padicabvf  24323  padicabvcxp  24324  mirval  24551  wwlknprop  25250  chscllem4  27119  brafnmul  27430  kbmul  27434  ofresid  28074  ofoprabco  28098  fcobijfs  28145  gsummpt2d  28373  gsummptres  28377  fzto1st1  28445  fzto1st  28446  mdetpmtr1  28479  mdetlap  28488  xrge0mulc1cn  28577  esumval  28697  esumsnf  28715  esumpcvgval  28729  esumcvg  28737  esumcvgsum  28739  esumsup  28740  ofcfeqd2  28752  meascnbl  28871  sitgval  28984  probmeasb  29080  cndprobprob  29088  dstfrvclim1  29127  ballotlemfval  29139  ballotlemsval  29158  ballotlemieq  29166  ofccat  29208  plymul02  29214  plymulx0  29215  plymulx  29216  signsplypnf  29218  signstfv  29231  signstfvn  29237  signstfvp  29239  ptpcon  29735  cvmliftlem6  29792  cvmliftphtlem  29819  cvmlift3lem5  29825  elmrsubrn  29937  msubfval  29941  msubco  29948  divcnvlin  30145  bj-finsumval0  31438  poimirlem3  31637  poimirlem15  31649  poimirlem16  31650  poimirlem17  31651  poimirlem19  31653  poimirlem20  31654  broucube  31668  ovoliunnfl  31676  voliunnfl  31678  volsupnfl  31679  mbfposadd  31682  itg2addnclem  31687  itg2addnclem3  31689  itg2addnc  31690  itgaddnclem2  31695  itgaddnc  31696  iblsubnc  31697  itgsubnc  31698  itgmulc2nclem1  31702  itgmulc2nclem2  31703  itgmulc2nc  31704  itgabsnc  31705  ftc1cnnclem  31709  ftc1anclem3  31713  ftc1anclem5  31715  ftc1anclem6  31716  ftc1anclem8  31718  ftc1anc  31719  ftc2nc  31720  areacirclem1  31726  areacirclem2  31727  areacirclem4  31729  areacirc  31731  upixp  31750  mzpsubst  35289  mzprename  35290  mzpcompact2lem  35292  eldioph2  35303  rabdiophlem2  35344  mendlmod  35748  mendassa  35749  areaquad  35790  hashnzfzclim  36298  expgrowthi  36309  expgrowth  36311  uzmptshftfval  36322  dvradcnv2  36323  binomcxplemrat  36326  binomcxplemfrat  36327  binomcxplemradcnv  36328  binomcxplemdvbinom  36329  binomcxplemcvg  36330  binomcxplemdvsum  36331  binomcxplemnotnn0  36332  mulc1cncfg  37229  expcnfg  37233  clim1fr1  37241  divcnvg  37269  sublimc  37295  reclimc  37296  divlimc  37299  cncfmptssg  37309  negcncfg  37320  divcncf  37323  cncficcgt0  37328  fprodcncf  37341  dvrecg  37344  dvsinax  37345  dvmptdiv  37351  dvasinbx  37354  dvdivf  37356  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  dvnmptdivc  37372  dvxpaek  37374  dvnxpaek  37376  dvnmul  37377  dvnprodlem2  37381  ibliccsinexp  37386  itgsinexplem1  37389  itgsinexp  37390  iblempty  37401  itgcoscmulx  37405  itgsincmulx  37410  itgioocnicc  37413  iblcncfioo  37414  itgsbtaddcnst  37418  stoweidlem4  37423  stirlinglem5  37499  dirkerval  37512  dirkertrigeq  37522  dirkeritg  37523  dirkercncflem2  37525  dirkercncflem4  37527  fourierdlem16  37544  fourierdlem18  37546  fourierdlem21  37549  fourierdlem22  37550  fourierdlem28  37556  fourierdlem39  37567  fourierdlem40  37568  fourierdlem41  37569  fourierdlem53  37581  fourierdlem56  37584  fourierdlem57  37585  fourierdlem60  37588  fourierdlem61  37589  fourierdlem68  37596  fourierdlem73  37601  fourierdlem74  37602  fourierdlem75  37603  fourierdlem76  37604  fourierdlem78  37606  fourierdlem81  37609  fourierdlem82  37610  fourierdlem83  37611  fourierdlem84  37612  fourierdlem85  37613  fourierdlem88  37616  fourierdlem90  37618  fourierdlem92  37620  fourierdlem93  37621  fourierdlem95  37623  fourierdlem97  37625  fourierdlem101  37629  fourierdlem103  37631  fourierdlem104  37632  fourierdlem111  37639  fourierdlem112  37640  sqwvfoura  37650  sqwvfourb  37651  fouriersw  37653  elaa2lem  37655  etransclem4  37660  etransclem17  37673  etransclem18  37674  etransclem32  37688  etransclem46  37702  sge0z  37741  sge0revalmpt  37744  sge0tsms  37746  sge0sup  37757  sge0iunmptlemre  37781  sge0iun  37785  ismeannd  37804  psmeasurelem  37807  caratheodory  37848  fdmdifeqresdif  38873  ply1mulgsumlem2  38929  lincvalsc0  38964  linc0scn0  38966  lincdifsn  38967  lincsum  38972  lincscm  38973  lindslinindimp2lem4  39004  lindslinindsimp2lem5  39005  lincresunit3lem2  39023  aacllem  39291