Theorem mpteq2dva 4523

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1383   e. wcel 1804   |-> cmpt 4495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-opab 4496  df-mpt 4497

This theorem is referenced by:  mpteq2dv  4524  2fvcoidd  6185  offval  6532  offval2  6541  caofinvl  6552  caofcom  6557  caofass  6559  caofdi  6561  caofdir  6562  caonncan  6563  curry1  6877  curry2  6880  mpt2curryd  7000  pw2f1olem  7623  mapxpen  7685  xpmapenlem  7686  cantnfp1  8103  cantnflem1d  8110  cantnflem1  8111  cantnfp1OLD  8129  cantnflem1dOLD  8133  cantnflem1OLD  8134  cnfcom2lem  8148  cnfcom2lemOLD  8156  dfac12lem1  8526  seqof  12146  seqof2  12147  swrd0val  12630  swrdswrd  12667  repswswrd  12738  repswrevw  12740  revco  12782  ccatco  12783  repsco  12787  lo1eq  13373  rlimeq  13374  lo1mul2  13433  o1dif  13434  lo1sub  13435  rlimdiv  13450  caucvgr  13480  sumeq1  13493  fsumrlim  13607  fsumo1  13608  climfsum  13616  geomulcvg  13667  vdwlem8  14488  restid2  14810  pwsplusgval  14869  pwsmulrval  14870  pwsvscafval  14873  qusin  14923  xpsaddlem  14954  xpsvsca  14958  catidd  15059  fuclid  15314  fucrid  15315  fucass  15316  setcepi  15394  prf1st  15452  prf2nd  15453  1st2ndprf  15454  curfcl  15480  curfuncf  15486  diag2  15493  curf2ndf  15495  hof2val  15504  hofcllem  15506  hofcl  15507  yonedalem4a  15523  yonedalem4c  15525  yonedalem3b  15527  yonedainv  15529  yonffthlem  15530  prdsidlem  15931  prdsmndd  15932  pwsco2mhm  15981  frmdup3lem  16013  frmdup3  16014  grpinvpropd  16092  prdsinvlem  16157  pwsinvg  16161  pwssub  16162  galactghm  16407  cayleylem1  16416  pmtrprfval  16491  sylow1lem2  16598  sylow3lem1  16626  efginvrel1  16725  frgpup3lem  16774  frgpup3  16775  prdscmnd  16846  iscyggen  16862  gsumval3OLD  16887  gsumval3  16890  gsumcllem  16891  gsumcllemOLD  16892  gsumzsplit  16923  gsumzsplitOLD  16924  gsumsub  16953  gsumsubOLD  16954  gsummptf1o  16969  gsum2d  16978  gsum2dOLD  16979  gsum2d2  16981  gsumxp  16983  gsumxpOLD  16985  prdsgsum  16986  prdsgsumOLD  16987  telgsumfz  16998  telgsumfz0  17000  telgsum  17002  dprdfsub  17040  dprdfeq0  17041  dprdfsubOLD  17047  dprdfeq0OLD  17048  dprddisj2  17066  dprddisj2OLD  17067  dprd2d2  17072  dpjidcl  17086  dpjidclOLD  17093  ablfaclem2  17116  ablfac2  17119  srgbinomlem3  17172  srgbinomlem4  17173  srgbinomlem  17174  gsumdixpOLD  17236  gsumdixp  17237  prdsmgp  17238  prdsringd  17240  prdslmodd  17594  asclpropd  17974  psrass1lem  18008  psrlinv  18029  psrass1  18039  psrdi  18040  psrdir  18041  psrass23l  18042  psrcom  18043  psrass23  18044  resspsrmul  18051  mplsubrglem  18079  mplsubrglemOLD  18080  mplmonmul  18105  mplcoe1  18106  mplcoe5  18110  mplcoe2OLD  18112  mplcoe4  18147  evlslem3  18162  evlslem1  18163  psrplusgpropd  18256  psropprmul  18258  coe1mul2  18289  coe1tm  18293  coe1tmmul2  18296  coe1tmmul  18297  coe1pwmul  18299  cply1mul  18314  ply1coe  18316  ply1coeOLD  18317  eqcoe1ply1eq  18318  lply1binomsc  18328  evl1gsummon  18380  mulgrhm2  18511  mulgrhm2OLD  18514  frgpcyg  18590  evpmodpmf1o  18610  phlpropd  18668  frlmphl  18790  uvcresum  18802  frlmup1  18810  mamures  18870  grpvrinv  18876  mhmvlin  18877  mamuass  18882  mamudi  18883  mamudir  18884  mamuvs1  18885  mamuvs2  18886  mpt2matmul  18926  mamutpos  18938  madetsumid  18941  dmatmul  18977  scmatscm  18993  1mavmul  19028  mavmulass  19029  mvmumamul1  19034  mulmarep1gsum1  19053  mulmarep1gsum2  19054  mdetleib2  19068  mdetfval1  19070  mdet0pr  19072  mdetdiag  19079  mdetdiagid  19080  mdetrlin  19082  mdetrsca  19083  mdetralt  19088  mdetunilem9  19100  gsummatr01  19139  smadiadetlem1a  19143  smadiadetlem3  19148  smadiadetlem4  19149  cpmatmcllem  19197  mat2pmatmul  19210  decpmatmullem  19250  decpmatmul  19251  pmatcollpw1lem2  19254  pmatcollpw  19260  pmatcollpw3lem  19262  pmatcollpwscmat  19270  idpm2idmp  19280  mp2pm2mplem3  19287  mp2pm2mplem4  19288  mp2pm2mplem5  19289  mp2pm2mp  19290  pm2mpghm  19295  pm2mpmhmlem2  19298  monmat2matmon  19303  pm2mp  19304  chpdmat  19320  chpscmat  19321  chpscmatgsumbin  19323  chpscmatgsummon  19324  chp0mat  19325  chpidmat  19326  chfacfscmulgsum  19339  chfacfpmmulgsum  19343  chfacfpmmulgsum2  19344  cayhamlem1  19345  cpmidgsumm2pm  19348  cpmidpmat  19352  cpmadugsumlemB  19353  cpmadugsumlemC  19354  cpmadugsumlemF  19355  cpmadumatpoly  19362  cayhamlem3  19366  cayhamlem4  19367  cayleyhamilton0  19368  cayleyhamiltonALT  19370  neiptopnei  19611  neiptopreu  19612  ptcnplem  20100  cnmpt1t  20144  cnmpt12  20146  cnmptkp  20159  cnmptk1  20160  cnmpt1k  20161  cnmptkk  20162  cnmptk1p  20164  cnmpt2k  20167  qtopeu  20195  pt1hmeo  20285  ptunhmeo  20287  xkocnv  20293  xkohmeo  20294  flfcnp2  20486  cnmpt1plusg  20564  istgp2  20568  tmdmulg  20569  tgpmulg  20570  tmdgsum  20572  symgtgp  20578  subgtgp  20582  tgpconcomp  20589  prdstgpd  20601  tsmsmhm  20626  tsmsadd  20627  tsmssub  20629  tgptsmscls  20630  tsmssplit  20632  tsmsxplem1  20633  tsmsxplem2  20634  cnmpt1vsca  20674  tlmtgp  20676  ustuqtoplem  20720  utopsnneip  20729  ressprdsds  20852  metuvalOLD  21030  metuval  21031  nmfval2  21089  tngnm  21143  nmoeq0  21221  idnghm  21228  cnmpt1ds  21325  fsumcn  21352  expcn  21354  divccn  21355  divccncf  21388  negcncf  21400  copco  21496  pcopt  21500  pcopt2  21501  pcoass  21502  pi1xfrcnvlem  21534  cnmpt1ip  21665  rrxnm  21801  rrxds  21803  minveclem3b  21821  ovolctb  21879  ovoliunnul  21896  voliunlem3  21940  ovolfs2  21958  uniioombllem2  21970  vitalilem4  21998  vitalilem5  21999  ismbf  22015  mbfss  22031  mbfmulc2re  22033  mbfneg  22035  mbfpos  22036  mbfposb  22038  mbfadd  22046  mbfsub  22047  mbfmulc2  22048  mbfinf  22050  mbflimsup  22051  mbflimlem  22052  i1fpos  22091  i1fposd  22092  itg1climres  22099  mbfmul  22111  itg2mulc  22132  itg2i1fseq  22140  itg2cnlem1  22146  itg2cnlem2  22147  itgresr  22163  iblneg  22187  i1fibl  22192  itgitg1  22193  iblsub  22206  itgfsum  22211  itgmulc2lem1  22216  limcmpt  22265  limccnp  22273  limcco  22275  dvreslem  22291  dvres2lem  22292  dvidlem  22297  dvcnp2  22301  dvaddbr  22319  dvmulbr  22320  dvmulf  22324  dvcmulf  22326  dvcobr  22327  dvcof  22329  dvcjbr  22330  dvcj  22331  dvfre  22332  dvexp  22334  dvexp2  22335  dvrec  22336  dvmptcmul  22345  dvmptdivc  22346  dvmptneg  22347  dvmptsub  22348  dvmptre  22350  dvmptim  22351  dvmptfsum  22354  dvcnvlem  22355  dvcnv  22356  dvexp3  22357  dvef  22359  dvsincos  22360  dv11cn  22380  lhop2  22394  lhop  22395  ftc2  22423  itgparts  22426  itgsubstlem  22427  mdegfval  22438  mdegmullem  22456  ply1termlem  22578  plypow  22580  plyconst  22581  plyeq0lem  22585  plypf1  22587  plyaddlem1  22588  plymullem1  22589  coeeulem  22599  coeidlem  22612  plyco  22616  coeeq2  22617  0dgr  22620  0dgrb  22621  dgrcolem1  22648  dgrcolem2  22649  plycjlem  22651  dvply1  22658  dvply2g  22659  plydiveu  22672  plyremlem  22678  elqaalem3  22695  taylfval  22732  dvtaylp  22743  taylthlem1  22746  taylthlem2  22747  ulmshft  22763  mtestbdd  22778  iblulm  22780  itgulm2  22782  pserulm  22795  psercn2  22796  pserdvlem2  22801  pserdv  22802  pserdv2  22803  abelthlem1  22804  abelthlem3  22806  advlog  23013  advlogexp  23014  dvcxp1  23094  dvcxp2  23095  sqrtcn  23102  loglesqrt  23110  dvatan  23244  atantayl2  23247  atantayl3  23248  leibpi  23251  rlimcnp2  23274  efrlim  23277  dfef2  23278  cxp2lim  23284  divsqrtsumlem  23287  ftalem7  23330  basellem9  23340  muinv  23447  logfacrlim  23477  logexprlim  23478  dchrmulid2  23505  dchrinvcl  23506  lgseisenlem3  23604  lgseisenlem4  23605  chtppilimlem2  23637  chebbnd2  23640  chpchtlim  23642  chpo1ub  23643  rpvmasumlem  23650  dchrmusumlema  23656  dchrvmasumlem1  23658  dchrvmasumiflem2  23665  dchrisum0fno1  23674  rpvmasum2  23675  dchrisum0lema  23677  dchrisum0lem1  23679  dchrisum0lem2a  23680  dchrisum0lem2  23681  dchrisum0  23683  dchrmusumlem  23685  dchrvmasumlem  23686  rpvmasum  23689  rplogsum  23690  logdivsum  23696  mulog2sumlem3  23699  vmalogdivsum2  23701  vmalogdivsum  23702  2vmadivsumlem  23703  logsqvma2  23706  log2sumbnd  23707  selberglem2  23709  selberg3lem1  23720  selberg3  23722  selberg4lem1  23723  selberg4  23724  pntrsumo1  23728  selberg3r  23732  selberg4r  23733  selberg34r  23734  pntrlog2bndlem2  23741  pntrlog2bndlem4  23743  pntrlog2bndlem5  23744  pntrlog2bndlem6  23746  padicabvf  23794  padicabvcxp  23795  mirval  24014  wwlknprop  24664  chscllem4  26536  brafnmul  26848  kbmul  26852  ofresid  27460  ofoprabco  27483  fcobijfs  27527  xrge0mulc1cn  27901  esumval  28035  esumsn  28050  esumpcvgval  28062  esumcvg  28070  ofcfeqd2  28078  meascnbl  28168  sitgval  28252  probmeasb  28347  cndprobprob  28355  dstfrvclim1  28394  ballotlemfval  28406  ballotlemsval  28425  ballotlemieq  28433  ofccat  28475  plymul02  28481  plymulx0  28482  plymulx  28483  signsplypnf  28485  signstfv  28498  signstfvn  28504  signstfvp  28506  lgamgulmlem2  28550  lgamgulm2  28556  lgamcvglem  28560  gamcvg2lem  28579  ptpcon  28656  cvmliftlem6  28713  cvmliftphtlem  28740  cvmlift3lem5  28746  elmrsubrn  28858  msubfval  28862  msubco  28869  divcnvlin  29096  ovoliunnfl  30032  voliunnfl  30034  volsupnfl  30035  mbfposadd  30038  itg2addnclem  30042  itg2addnclem3  30044  itg2addnc  30045  itgaddnclem2  30050  itgaddnc  30051  iblsubnc  30052  itgsubnc  30053  itgmulc2nclem1  30057  itgmulc2nclem2  30058  itgmulc2nc  30059  itgabsnc  30060  ftc1cnnclem  30064  ftc1anclem3  30068  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem8  30073  ftc1anc  30074  ftc2nc  30075  dvcncxp1  30076  areacirclem1  30083  areacirclem2  30084  areacirclem4  30086  areacirc  30088  upixp  30196  mzpsubst  30657  mzprename  30658  mzpcompact2lem  30660  eldioph2  30671  rabdiophlem2  30711  mendlmod  31118  mendassa  31119  areaquad  31160  hashnzfzclim  31203  expgrowthi  31214  expgrowth  31216  mulc1cncfg  31537  expcnfg  31540  clim1fr1  31561  divcnvg  31587  sublimc  31612  reclimc  31613  divlimc  31616  cncfmptssg  31626  negcncfg  31637  divcncf  31640  cncficcgt0  31645  fprodcncf  31658  dvrecg  31661  dvsinax  31662  dvmptdiv  31668  dvasinbx  31671  dvdivf  31673  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnmptdivc  31689  dvxpaek  31691  dvnxpaek  31693  dvnmul  31694  dvnprodlem2  31698  ibliccsinexp  31703  itgsinexplem1  31706  itgsinexp  31707  iblempty  31718  itgcoscmulx  31722  itgsincmulx  31727  itgioocnicc  31730  iblcncfioo  31731  itgsbtaddcnst  31735  stoweidlem4  31740  stirlinglem5  31814  dirkerval  31827  dirkertrigeq  31837  dirkeritg  31838  dirkercncflem2  31840  dirkercncflem4  31842  fourierdlem16  31859  fourierdlem18  31861  fourierdlem21  31864  fourierdlem22  31865  fourierdlem28  31871  fourierdlem39  31882  fourierdlem40  31883  fourierdlem41  31884  fourierdlem53  31896  fourierdlem56  31899  fourierdlem57  31900  fourierdlem60  31903  fourierdlem61  31904  fourierdlem68  31911  fourierdlem73  31916  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem78  31921  fourierdlem81  31924  fourierdlem82  31925  fourierdlem83  31926  fourierdlem84  31927  fourierdlem85  31928  fourierdlem88  31931  fourierdlem90  31933  fourierdlem92  31935  fourierdlem93  31936  fourierdlem95  31938  fourierdlem97  31940  fourierdlem101  31944  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem112  31955  sqwvfoura  31965  sqwvfourb  31966  fouriersw  31968  elaa2lem  31970  etransclem4  31975  etransclem17  31988  etransclem18  31989  etransclem32  32003  etransclem46  32017  fdmdifeqresdif  32799  ply1mulgsumlem2  32857  lincvalsc0  32892  linc0scn0  32894  lincdifsn  32895  lincsum  32900  lincscm  32901  lindslinindimp2lem4  32932  lindslinindsimp2lem5  32933  lincresunit3lem2  32951  bj-finsumval0  34538