Theorem mpteq2dva 4533

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   e. wcel 1767   |-> cmpt 4505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-opab 4506  df-mpt 4507

This theorem is referenced by:  mpteq2dv  4534  fmptapd  6083  2fvcoidd  6186  offval  6529  offval2  6538  caofinvl  6549  caofcom  6554  caofass  6556  caofdi  6558  caofdir  6559  caonncan  6560  curry1  6872  curry2  6875  mpt2curryd  6995  pw2f1olem  7618  mapxpen  7680  xpmapenlem  7681  cantnfp1  8096  cantnflem1d  8103  cantnflem1  8104  cantnfp1OLD  8122  cantnflem1dOLD  8126  cantnflem1OLD  8127  cnfcom2lem  8141  cnfcom2lemOLD  8149  dfac12lem1  8519  seqof  12127  seqof2  12128  swrd0val  12605  swrdswrd  12642  repswswrd  12713  repswrevw  12715  revco  12757  ccatco  12758  repsco  12762  lo1eq  13347  rlimeq  13348  lo1mul2  13407  o1dif  13408  lo1sub  13409  rlimdiv  13424  caucvgr  13454  sumeq1  13467  fsumrlim  13581  fsumo1  13582  climfsum  13590  geomulcvg  13641  vdwlem8  14358  restid2  14679  pwsplusgval  14738  pwsmulrval  14739  pwsvscafval  14742  divsin  14792  xpsaddlem  14823  xpsvsca  14827  catidd  14928  fuclid  15186  fucrid  15187  fucass  15188  setcepi  15266  prf1st  15324  prf2nd  15325  1st2ndprf  15326  curfcl  15352  curfuncf  15358  diag2  15365  curf2ndf  15367  hof2val  15376  hofcllem  15378  hofcl  15379  yonedalem4a  15395  yonedalem4c  15397  yonedalem3b  15399  yonedainv  15401  yonffthlem  15402  prdsidlem  15763  prdsmndd  15764  pwsco2mhm  15809  frmdup3  15854  grpinvpropd  15911  prdsinvlem  15975  pwsinvg  15979  pwssub  15980  galactghm  16220  cayleylem1  16229  pmtrprfval  16305  sylow1lem2  16412  sylow3lem1  16440  efginvrel1  16539  frgpup3lem  16588  frgpup3  16589  prdscmnd  16657  iscyggen  16671  gsumval3OLD  16696  gsumval3  16699  gsumcllem  16700  gsumcllemOLD  16701  gsumzsplit  16732  gsumzsplitOLD  16733  gsummptshft  16744  gsumsub  16762  gsumsubOLD  16763  gsummptf1o  16778  gsum2d  16787  gsum2dOLD  16788  gsum2d2  16790  gsumxp  16792  gsumxpOLD  16794  prdsgsum  16795  prdsgsumOLD  16796  telgsumfz  16807  telgsumfz0  16809  telgsum  16811  dprdfsub  16848  dprdfeq0  16849  dprdfsubOLD  16855  dprdfeq0OLD  16856  dprddisj2  16874  dprddisj2OLD  16875  dprd2d2  16880  dpjidcl  16894  dpjidclOLD  16901  ablfaclem2  16924  ablfac2  16927  srgbinomlem3  16978  srgbinomlem4  16979  srgbinomlem  16980  gsumdixpOLD  17038  gsumdixp  17039  prdsmgp  17040  prdsrngd  17042  prdslmodd  17395  asclpropd  17763  psrass1lem  17797  psrlinv  17818  psrass1  17828  psrdi  17829  psrdir  17830  psrass23l  17831  psrcom  17832  psrass23  17833  resspsrmul  17840  mplsubrglem  17868  mplsubrglemOLD  17869  mplmonmul  17894  mplcoe1  17895  mplcoe5  17899  mplcoe2OLD  17901  mplcoe4  17936  evlslem3  17951  evlslem1  17952  psrplusgpropd  18045  psropprmul  18047  coe1mul2  18078  coe1tm  18082  coe1tmmul2  18085  coe1tmmul  18086  coe1pwmul  18088  cply1mul  18103  ply1coe  18105  ply1coeOLD  18106  eqcoe1ply1eq  18107  lply1binomsc  18117  evl1gsummon  18169  mulgrhm2  18297  mulgrhm2OLD  18300  frgpcyg  18376  evpmodpmf1o  18396  phlpropd  18454  frlmphl  18576  uvcresum  18588  frlmup1  18596  mamures  18656  grpvrinv  18662  mhmvlin  18663  mamuass  18668  mamudi  18669  mamudir  18670  mamuvs1  18671  mamuvs2  18672  mpt2matmul  18712  mamutpos  18724  madetsumid  18727  dmatmul  18763  scmatscm  18779  1mavmul  18814  mavmulass  18815  mvmumamul1  18820  mulmarep1gsum1  18839  mulmarep1gsum2  18840  mdetleib2  18854  mdetfval1  18856  mdet0pr  18858  mdetdiag  18865  mdetdiagid  18866  mdetrlin  18868  mdetrsca  18869  mdetralt  18874  mdetunilem9  18886  gsummatr01  18925  smadiadetlem1a  18929  smadiadetlem3  18934  smadiadetlem4  18935  cpmatmcllem  18983  mat2pmatmul  18996  decpmatmullem  19036  decpmatmul  19037  pmatcollpw1lem2  19040  pmatcollpw  19046  pmatcollpw3lem  19048  pmatcollpwscmat  19056  idpm2idmp  19066  mp2pm2mplem3  19073  mp2pm2mplem4  19074  mp2pm2mplem5  19075  mp2pm2mp  19076  pm2mpghm  19081  pm2mpmhmlem2  19084  monmat2matmon  19089  pm2mp  19090  chpdmat  19106  chpscmat  19107  chpscmatgsumbin  19109  chpscmatgsummon  19110  chp0mat  19111  chpidmat  19112  chfacfscmulgsum  19125  chfacfpmmulgsum  19129  chfacfpmmulgsum2  19130  cayhamlem1  19131  cpmidgsumm2pm  19134  cpmidpmat  19138  cpmadugsumlemB  19139  cpmadugsumlemC  19140  cpmadugsumlemF  19141  cpmadumatpoly  19148  cayhamlem3  19152  cayhamlem4  19153  cayleyhamilton0  19154  cayleyhamiltonALT  19156  neiptopnei  19396  neiptopreu  19397  ptcnplem  19854  cnmpt1t  19898  cnmpt12  19900  cnmptkp  19913  cnmptk1  19914  cnmpt1k  19915  cnmptkk  19916  cnmptk1p  19918  cnmpt2k  19921  qtopeu  19949  pt1hmeo  20039  ptunhmeo  20041  xkocnv  20047  xkohmeo  20048  flfcnp2  20240  cnmpt1plusg  20318  istgp2  20322  tmdmulg  20323  tgpmulg  20324  tmdgsum  20326  symgtgp  20332  subgtgp  20336  tgpconcomp  20343  prdstgpd  20355  tsmsmhm  20380  tsmsadd  20381  tsmssub  20383  tgptsmscls  20384  tsmssplit  20386  tsmsxplem1  20387  tsmsxplem2  20388  cnmpt1vsca  20428  tlmtgp  20430  ustuqtoplem  20474  utopsnneip  20483  ressprdsds  20606  metuvalOLD  20784  metuval  20785  nmfval2  20843  tngnm  20897  nmoeq0  20975  idnghm  20982  cnmpt1ds  21079  fsumcn  21106  expcn  21108  divccn  21109  divccncf  21142  negcncf  21154  copco  21250  pcopt  21254  pcopt2  21255  pcoass  21256  pi1xfrcnvlem  21288  cnmpt1ip  21419  rrxnm  21555  rrxds  21557  minveclem3b  21575  ovolctb  21633  ovoliunnul  21650  voliunlem3  21694  ovolfs2  21712  uniioombllem2  21724  vitalilem4  21752  vitalilem5  21753  ismbf  21769  mbfss  21785  mbfmulc2re  21787  mbfneg  21789  mbfpos  21790  mbfposb  21792  mbfadd  21800  mbfsub  21801  mbfmulc2  21802  mbfinf  21804  mbflimsup  21805  mbflimlem  21806  i1fpos  21845  i1fposd  21846  itg1climres  21853  mbfmul  21865  itg2mulc  21886  itg2i1fseq  21894  itg2cnlem1  21900  itg2cnlem2  21901  itgresr  21917  iblneg  21941  i1fibl  21946  itgitg1  21947  iblsub  21960  itgfsum  21965  itgmulc2lem1  21970  limcmpt  22019  limccnp  22027  limcco  22029  dvreslem  22045  dvres2lem  22046  dvidlem  22051  dvcnp2  22055  dvaddbr  22073  dvmulbr  22074  dvmulf  22078  dvcmulf  22080  dvcobr  22081  dvcof  22083  dvcjbr  22084  dvcj  22085  dvfre  22086  dvexp  22088  dvexp2  22089  dvrec  22090  dvmptcmul  22099  dvmptdivc  22100  dvmptneg  22101  dvmptsub  22102  dvmptre  22104  dvmptim  22105  dvmptfsum  22108  dvcnvlem  22109  dvcnv  22110  dvexp3  22111  dvef  22113  dvsincos  22114  dv11cn  22134  lhop2  22148  lhop  22149  ftc2  22177  itgparts  22180  itgsubstlem  22181  mdegfval  22192  mdegmullem  22210  ply1termlem  22332  plypow  22334  plyconst  22335  plyeq0lem  22339  plypf1  22341  plyaddlem1  22342  plymullem1  22343  coeeulem  22353  coeidlem  22366  plyco  22370  coeeq2  22371  0dgr  22374  0dgrb  22375  dgrcolem1  22401  dgrcolem2  22402  plycjlem  22404  dvply1  22411  dvply2g  22412  plydiveu  22425  plyremlem  22431  elqaalem3  22448  taylfval  22485  dvtaylp  22496  taylthlem1  22499  taylthlem2  22500  ulmshft  22516  mtestbdd  22531  iblulm  22533  itgulm2  22535  pserulm  22548  psercn2  22549  pserdvlem2  22554  pserdv  22555  pserdv2  22556  abelthlem1  22557  abelthlem3  22559  advlog  22760  advlogexp  22761  dvcxp1  22841  dvcxp2  22842  sqrtcn  22849  loglesqrt  22857  dvatan  22991  atantayl2  22994  atantayl3  22995  leibpi  22998  rlimcnp2  23021  efrlim  23024  dfef2  23025  cxp2lim  23031  divsqrtsumlem  23034  ftalem7  23077  basellem9  23087  muinv  23194  logfacrlim  23224  logexprlim  23225  dchrmulid2  23252  dchrinvcl  23253  lgseisenlem3  23351  lgseisenlem4  23352  chtppilimlem2  23384  chebbnd2  23387  chpchtlim  23389  chpo1ub  23390  rpvmasumlem  23397  dchrmusumlema  23403  dchrvmasumlem1  23405  dchrvmasumiflem2  23412  dchrisum0fno1  23421  rpvmasum2  23422  dchrisum0lema  23424  dchrisum0lem1  23426  dchrisum0lem2a  23427  dchrisum0lem2  23428  dchrisum0  23430  dchrmusumlem  23432  dchrvmasumlem  23433  rpvmasum  23436  rplogsum  23437  logdivsum  23443  mulog2sumlem3  23446  vmalogdivsum2  23448  vmalogdivsum  23449  2vmadivsumlem  23450  logsqvma2  23453  log2sumbnd  23454  selberglem2  23456  selberg3lem1  23467  selberg3  23469  selberg4lem1  23470  selberg4  23471  pntrsumo1  23475  selberg3r  23479  selberg4r  23480  selberg34r  23481  pntrlog2bndlem2  23488  pntrlog2bndlem4  23490  pntrlog2bndlem5  23491  pntrlog2bndlem6  23493  padicabvf  23541  padicabvcxp  23542  mirval  23746  wwlknprop  24359  chscllem4  26231  brafnmul  26543  kbmul  26547  ofresid  27152  ofoprabco  27174  fcobijfs  27218  gsumsn2  27429  xrge0mulc1cn  27556  esumval  27694  esumsn  27709  esumpcvgval  27721  esumcvg  27729  ofcfeqd2  27737  meascnbl  27827  sitgval  27911  probmeasb  28006  cndprobprob  28014  dstfrvclim1  28053  ballotlemfval  28065  ballotlemsval  28084  ballotlemieq  28092  ofccat  28134  plymul02  28140  plymulx0  28141  plymulx  28142  signsplypnf  28144  signstfv  28157  signstfvn  28163  signstfvp  28165  lgamgulmlem2  28209  lgamgulm2  28215  lgamcvglem  28219  gamcvg2lem  28238  ptpcon  28315  cvmliftlem6  28372  cvmliftphtlem  28399  cvmlift3lem5  28405  divcnvlin  28592  ovoliunnfl  29631  voliunnfl  29633  volsupnfl  29634  mbfposadd  29637  itg2addnclem  29641  itg2addnclem3  29643  itg2addnc  29644  itgaddnclem2  29649  itgaddnc  29650  iblsubnc  29651  itgsubnc  29652  itgmulc2nclem1  29656  itgmulc2nclem2  29657  itgmulc2nc  29658  itgabsnc  29659  ftc1cnnclem  29663  ftc1anclem3  29667  ftc1anclem5  29669  ftc1anclem6  29670  ftc1anclem8  29672  ftc1anc  29673  ftc2nc  29674  dvcncxp1  29675  areacirclem1  29682  areacirclem2  29683  areacirclem4  29685  areacirc  29687  upixp  29821  mzpsubst  30283  mzprename  30284  mzpcompact2lem  30286  eldioph2  30297  rabdiophlem2  30337  mendlmod  30747  mendassa  30748  areaquad  30789  hashnzfzclim  30827  expgrowthi  30838  expgrowth  30840  mulc1cncfg  31139  expcnfg  31142  clim1fr1  31143  divcnvg  31169  sublimc  31194  reclimc  31195  divlimc  31198  cncfmptssg  31208  negcncfg  31219  divcncf  31222  cncficcgt0  31227  dvrecg  31240  dvsinax  31241  dvmptdiv  31247  dvasinbx  31250  dvdivf  31252  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  ibliccsinexp  31268  itgsinexplem1  31271  itgsinexp  31272  iblempty  31283  itgcoscmulx  31287  itgsincmulx  31292  itgioocnicc  31295  iblcncfioo  31296  itgsbtaddcnst  31300  stoweidlem4  31304  stirlinglem5  31378  dirkerval  31391  dirkertrigeq  31401  dirkeritg  31402  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem16  31423  fourierdlem18  31425  fourierdlem21  31428  fourierdlem22  31429  fourierdlem28  31435  fourierdlem39  31446  fourierdlem40  31447  fourierdlem41  31448  fourierdlem53  31460  fourierdlem56  31463  fourierdlem57  31464  fourierdlem60  31467  fourierdlem61  31468  fourierdlem68  31475  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem78  31485  fourierdlem81  31488  fourierdlem82  31489  fourierdlem83  31490  fourierdlem84  31491  fourierdlem85  31492  fourierdlem88  31495  fourierdlem90  31497  fourierdlem92  31499  fourierdlem93  31500  fourierdlem95  31502  fourierdlem97  31504  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  sqwvfoura  31529  sqwvfourb  31530  fouriersw  31532  fdmdifeqresdif  31995  ply1mulgsumlem2  32060  lincvalsc0  32095  linc0scn0  32097  lincdifsn  32098  lincsum  32103  lincscm  32104  lindslinindimp2lem4  32135  lindslinindsimp2lem5  32136  lincresunit3lem2  32154  bj-finsumval0  33735