Theorem mpteq2dva 4448

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-ral 2714  df-opab 4421  df-mpt 4422

This theorem is referenced by:  mpteq2dv  4449  2fvcoidd  6149  offval  6491  offval2  6501  caofinvl  6511  caofcom  6516  caofass  6518  caofdi  6520  caofdir  6521  caonncan  6522  curry1  6838  curry2  6841  mpt2curryd  6966  pw2f1olem  7624  mapxpen  7686  xpmapenlem  7687  cantnfp1  8133  cantnflem1d  8140  cantnflem1  8141  cnfcom2lem  8153  dfac12lem1  8519  seqof  12215  seqof2  12216  swrd0val  12718  swrdswrd  12757  repswswrd  12828  repswrevw  12830  revco  12872  ccatco  12873  repsco  12877  lo1eq  13570  rlimeq  13571  lo1mul2  13630  o1dif  13631  lo1sub  13632  rlimdiv  13647  caucvgr  13679  sumeq1  13693  fsumrlim  13809  fsumo1  13810  climfsum  13818  geomulcvg  13870  vdwlem8  14876  prmgapprmo  14971  restid2  15267  pwsplusgval  15326  pwsmulrval  15327  pwsvscafval  15330  qusin  15388  xpsaddlem  15419  xpsvsca  15423  catidd  15524  fuclid  15809  fucrid  15810  fucass  15811  setcepi  15921  prf1st  16027  prf2nd  16028  1st2ndprf  16029  curfcl  16055  curfuncf  16061  diag2  16068  curf2ndf  16070  hof2val  16079  hofcllem  16081  hofcl  16082  yonedalem4a  16098  yonedalem4c  16100  yonedalem3b  16102  yonedainv  16104  yonffthlem  16105  prdsidlem  16506  prdsmndd  16507  pwsco2mhm  16556  frmdup3lem  16588  frmdup3  16589  grpinvpropd  16667  prdsinvlem  16732  pwsinvg  16736  pwssub  16737  galactghm  16982  cayleylem1  16991  pmtrprfval  17066  sylow1lem2  17189  sylow3lem1  17217  efginvrel1  17316  frgpup3lem  17365  frgpup3  17366  prdscmnd  17437  iscyggen  17453  gsumval3  17479  gsumcllem  17480  gsumzsplit  17498  gsumsub  17519  gsummptf1o  17533  gsum2d  17542  gsum2d2  17544  gsumxp  17546  prdsgsum  17548  telgsumfz  17558  telgsumfz0  17560  telgsum  17562  dprdfsub  17592  dprdfeq0  17593  dprddisj2  17610  dprd2d2  17615  dpjidcl  17629  ablfaclem2  17657  ablfac2  17660  srgbinomlem3  17713  srgbinomlem4  17714  srgbinomlem  17715  gsumdixp  17775  prdsmgp  17776  prdsringd  17778  prdslmodd  18130  asclpropd  18508  psrass1lem  18539  psrlinv  18559  psrass1  18567  psrdi  18568  psrdir  18569  psrass23l  18570  psrcom  18571  psrass23  18572  resspsrmul  18579  mplsubrglem  18601  mplmonmul  18626  mplcoe1  18627  mplcoe5  18630  mplcoe4  18664  evlslem3  18675  evlslem1  18676  psrplusgpropd  18767  psropprmul  18769  coe1mul2  18800  coe1tm  18804  coe1tmmul2  18807  coe1tmmul  18808  coe1pwmul  18810  cply1mul  18825  ply1coe  18827  ply1coeOLD  18828  eqcoe1ply1eq  18829  lply1binomsc  18839  evl1gsummon  18891  mulgrhm2  19007  frgpcyg  19081  evpmodpmf1o  19101  phlpropd  19159  frlmphl  19276  uvcresum  19288  frlmup1  19293  mamures  19352  grpvrinv  19358  mhmvlin  19359  mamuass  19364  mamudi  19365  mamudir  19366  mamuvs1  19367  mamuvs2  19368  mpt2matmul  19408  mamutpos  19420  madetsumid  19423  dmatmul  19459  scmatscm  19475  1mavmul  19510  mavmulass  19511  mvmumamul1  19516  mulmarep1gsum1  19535  mulmarep1gsum2  19536  mdetleib2  19550  mdetfval1  19552  mdet0pr  19554  mdetdiag  19561  mdetdiagid  19562  mdetrlin  19564  mdetrsca  19565  mdetralt  19570  mdetunilem9  19582  gsummatr01  19621  smadiadetlem1a  19625  smadiadetlem3  19630  smadiadetlem4  19631  cpmatmcllem  19679  mat2pmatmul  19692  decpmatmullem  19732  decpmatmul  19733  pmatcollpw1lem2  19736  pmatcollpw  19742  pmatcollpw3lem  19744  pmatcollpwscmat  19752  idpm2idmp  19762  mp2pm2mplem3  19769  mp2pm2mplem4  19770  mp2pm2mplem5  19771  mp2pm2mp  19772  pm2mpghm  19777  pm2mpmhmlem2  19780  monmat2matmon  19785  pm2mp  19786  chpdmat  19802  chpscmat  19803  chpscmatgsumbin  19805  chpscmatgsummon  19806  chp0mat  19807  chpidmat  19808  chfacfscmulgsum  19821  chfacfpmmulgsum  19825  chfacfpmmulgsum2  19826  cayhamlem1  19827  cpmidgsumm2pm  19830  cpmidpmat  19834  cpmadugsumlemB  19835  cpmadugsumlemC  19836  cpmadugsumlemF  19837  cpmadumatpoly  19844  cayhamlem3  19848  cayhamlem4  19849  cayleyhamilton0  19850  cayleyhamiltonALT  19852  neiptopnei  20085  neiptopreu  20086  ptcnplem  20573  cnmpt1t  20617  cnmpt12  20619  cnmptkp  20632  cnmptk1  20633  cnmpt1k  20634  cnmptkk  20635  cnmptk1p  20637  cnmpt2k  20640  qtopeu  20668  pt1hmeo  20758  ptunhmeo  20760  xkocnv  20766  xkohmeo  20767  flfcnp2  20959  cnmpt1plusg  21039  istgp2  21043  tmdmulg  21044  tgpmulg  21045  tmdgsum  21047  symgtgp  21053  subgtgp  21057  tgpconcomp  21064  prdstgpd  21076  tsmsmhm  21097  tsmsadd  21098  tsmssub  21100  tgptsmscls  21101  tsmssplit  21103  tsmsxplem1  21104  tsmsxplem2  21105  cnmpt1vsca  21145  tlmtgp  21147  ustuqtoplem  21191  utopsnneip  21200  ressprdsds  21323  metuval  21501  nmfval2  21542  tngnm  21596  nmoeq0  21694  idnghm  21701  cnmpt1ds  21797  fsumcn  21839  expcn  21841  divccn  21842  divccncf  21875  negcncf  21887  copco  21986  pcopt  21990  pcopt2  21991  pcoass  21992  pi1xfrcnvlem  22024  cnmpt1ip  22155  rrxnm  22287  rrxds  22289  minveclem3b  22307  minveclem3bOLD  22319  ovolctb  22380  ovoliunnul  22397  voliunlem3  22442  ovolfs2  22460  uniioombllem2  22477  uniioombllem2OLD  22478  vitalilem4  22506  vitalilem5  22507  ismbf  22523  mbfss  22539  mbfmulc2re  22541  mbfneg  22543  mbfpos  22544  mbfposb  22546  mbfadd  22554  mbfsub  22555  mbfmulc2  22556  mbfinf  22558  mbfinfOLD  22559  mbflimsup  22560  mbflimsupOLD  22561  mbflimlem  22562  i1fpos  22601  i1fposd  22602  itg1climres  22609  mbfmul  22621  itg2mulc  22642  itg2i1fseq  22650  itg2cnlem1  22656  itg2cnlem2  22657  itgresr  22673  iblneg  22697  i1fibl  22702  itgitg1  22703  iblsub  22716  itgfsum  22721  itgmulc2lem1  22726  limcmpt  22775  limccnp  22783  limcco  22785  dvreslem  22801  dvres2lem  22802  dvidlem  22807  dvcnp2  22811  dvaddbr  22829  dvmulbr  22830  dvmulf  22834  dvcmulf  22836  dvcobr  22837  dvcof  22839  dvcjbr  22840  dvcj  22841  dvfre  22842  dvexp  22844  dvexp2  22845  dvrec  22846  dvmptcmul  22855  dvmptdivc  22856  dvmptneg  22857  dvmptsub  22858  dvmptre  22860  dvmptim  22861  dvmptfsum  22864  dvcnvlem  22865  dvcnv  22866  dvexp3  22867  dvef  22869  dvsincos  22870  dv11cn  22890  lhop2  22904  lhop  22905  ftc2  22933  itgparts  22936  itgsubstlem  22937  mdegfval  22948  mdegmullem  22964  ply1termlem  23094  plypow  23096  plyconst  23097  plyeq0lem  23101  plypf1  23103  plyaddlem1  23104  plymullem1  23105  coeeulem  23115  coeidlem  23128  plyco  23132  coeeq2  23133  0dgr  23136  0dgrb  23137  dgrcolem1  23164  dgrcolem2  23165  plycjlem  23167  dvply1  23174  dvply2g  23175  plydiveu  23188  plyremlem  23194  elqaalem3  23211  elqaalem3OLD  23214  taylfval  23251  dvtaylp  23262  taylthlem1  23265  taylthlem2  23266  ulmshft  23282  mtestbdd  23297  iblulm  23299  itgulm2  23301  pserulm  23314  psercn2  23315  pserdvlem2  23320  pserdv  23321  pserdv2  23322  abelthlem1  23323  abelthlem3  23325  advlog  23536  advlogexp  23537  dvcxp1  23617  dvcxp2  23618  dvcncxp1  23620  sqrtcn  23627  loglesqrt  23635  dvatan  23798  atantayl2  23801  atantayl3  23802  leibpi  23805  rlimcnp2  23829  efrlim  23832  dfef2  23833  cxp2lim  23839  divsqrtsumlem  23842  lgamgulmlem2  23892  lgamgulm2  23898  lgamcvglem  23902  gamcvg2lem  23921  ftalem7  23942  basellem9  23952  muinv  24059  logfacrlim  24089  logexprlim  24090  dchrmulid2  24117  dchrinvcl  24118  lgseisenlem3  24216  lgseisenlem4  24217  chtppilimlem2  24249  chebbnd2  24252  chpchtlim  24254  chpo1ub  24255  rpvmasumlem  24262  dchrmusumlema  24268  dchrvmasumlem1  24270  dchrvmasumiflem2  24277  dchrisum0fno1  24286  rpvmasum2  24287  dchrisum0lema  24289  dchrisum0lem1  24291  dchrisum0lem2a  24292  dchrisum0lem2  24293  dchrisum0  24295  dchrmusumlem  24297  dchrvmasumlem  24298  rpvmasum  24301  rplogsum  24302  logdivsum  24308  mulog2sumlem3  24311  vmalogdivsum2  24313  vmalogdivsum  24314  2vmadivsumlem  24315  logsqvma2  24318  log2sumbnd  24319  selberglem2  24321  selberg3lem1  24332  selberg3  24334  selberg4lem1  24335  selberg4  24336  pntrsumo1  24340  selberg3r  24344  selberg4r  24345  selberg34r  24346  pntrlog2bndlem2  24353  pntrlog2bndlem4  24355  pntrlog2bndlem5  24356  pntrlog2bndlem6  24358  padicabvf  24406  padicabvcxp  24407  mirval  24637  wwlknprop  25351  chscllem4  27230  brafnmul  27541  kbmul  27545  ofresid  28184  ofoprabco  28208  fcobijfs  28256  gsummpt2d  28490  gsummptres  28494  fzto1st1  28562  fzto1st  28563  mdetpmtr1  28596  mdetlap  28605  xrge0mulc1cn  28694  esumval  28814  esumsnf  28832  esumpcvgval  28846  esumcvg  28854  esumcvgsum  28856  esumsup  28857  ofcfeqd2  28869  meascnbl  28988  sitgval  29112  probmeasb  29210  cndprobprob  29218  dstfrvclim1  29257  ballotlemfval  29269  ballotlemsval  29288  ballotlemieq  29296  ballotlemsvalOLD  29326  ballotlemieqOLD  29334  ofccat  29376  plymul02  29382  plymulx0  29383  plymulx  29384  signsplypnf  29386  signstfv  29399  signstfvn  29405  signstfvp  29407  ptpcon  29903  cvmliftlem6  29960  cvmliftphtlem  29987  cvmlift3lem5  29993  elmrsubrn  30105  msubfval  30109  msubco  30116  divcnvlin  30313  bj-finsumval0  31609  poimirlem3  31850  poimirlem15  31862  poimirlem16  31863  poimirlem17  31864  poimirlem19  31866  poimirlem20  31867  broucube  31881  ovoliunnfl  31889  voliunnfl  31891  volsupnfl  31892  mbfposadd  31895  itg2addnclem  31900  itg2addnclem3  31902  itg2addnc  31903  itgaddnclem2  31908  itgaddnc  31909  iblsubnc  31910  itgsubnc  31911  itgmulc2nclem1  31915  itgmulc2nclem2  31916  itgmulc2nc  31917  itgabsnc  31918  ftc1cnnclem  31922  ftc1anclem3  31926  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anclem8  31931  ftc1anc  31932  ftc2nc  31933  areacirclem1  31939  areacirclem2  31940  areacirclem4  31942  areacirc  31944  upixp  31963  mzpsubst  35502  mzprename  35503  mzpcompact2lem  35505  eldioph2  35516  rabdiophlem2  35557  mendlmod  35972  mendassa  35973  areaquad  36014  hashnzfzclim  36584  expgrowthi  36595  expgrowth  36597  uzmptshftfval  36608  dvradcnv2  36609  binomcxplemrat  36612  binomcxplemfrat  36613  binomcxplemradcnv  36614  binomcxplemdvbinom  36615  binomcxplemcvg  36616  binomcxplemdvsum  36617  binomcxplemnotnn0  36618  mulc1cncfg  37550  expcnfg  37554  clim1fr1  37562  divcnvg  37590  sublimc  37616  reclimc  37617  divlimc  37620  cncfmptssg  37630  negcncfg  37641  divcncf  37644  cncficcgt0  37649  fprodcncf  37662  dvrecg  37665  dvsinax  37666  dvmptdiv  37672  dvasinbx  37675  dvdivf  37677  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  dvnmptdivc  37696  dvxpaek  37698  dvnxpaek  37700  dvnmul  37701  dvnprodlem2  37705  ibliccsinexp  37710  itgsinexplem1  37713  itgsinexp  37714  iblempty  37725  itgcoscmulx  37729  itgsincmulx  37734  itgioocnicc  37737  iblcncfioo  37738  itgsbtaddcnst  37742  stoweidlem4  37747  stirlinglem5  37823  dirkerval  37836  dirkertrigeq  37846  dirkeritg  37847  dirkercncflem2  37849  dirkercncflem4  37851  fourierdlem16  37868  fourierdlem18  37870  fourierdlem21  37873  fourierdlem22  37874  fourierdlem28  37880  fourierdlem39  37892  fourierdlem40  37893  fourierdlem41  37894  fourierdlem53  37906  fourierdlem56  37909  fourierdlem57  37910  fourierdlem60  37913  fourierdlem61  37914  fourierdlem68  37921  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem78  37931  fourierdlem81  37934  fourierdlem82  37935  fourierdlem83  37936  fourierdlem84  37937  fourierdlem85  37938  fourierdlem88  37941  fourierdlem90  37943  fourierdlem92  37945  fourierdlem93  37946  fourierdlem95  37948  fourierdlem97  37950  fourierdlem101  37954  fourierdlem103  37956  fourierdlem104  37957  fourierdlem111  37964  fourierdlem112  37965  sqwvfoura  37975  sqwvfourb  37976  fouriersw  37978  elaa2lem  37980  elaa2lemOLD  37981  etransclem4  37986  etransclem17  37999  etransclem18  38000  etransclem32  38014  etransclem46  38028  sge0z  38068  sge0revalmpt  38071  sge0tsms  38073  sge0sup  38084  sge0iunmptlemre  38108  sge0iun  38112  sge0xaddlem2  38127  ismeannd  38156  psmeasurelem  38159  caratheodory  38200  isomenndlem  38202  ovnval  38209  hoicvrrex  38225  ovnlecvr  38227  ovncvrrp  38233  ovn0lem  38234  ovnsubaddlem1  38239  hoidmv1lelem2  38261  hoidmv1le  38263  hoidmvlelem3  38266  ovnhoilem2  38271  ovnhoi  38272  fdmdifeqresdif  39716  ply1mulgsumlem2  39772  lincvalsc0  39807  linc0scn0  39809  lincdifsn  39810  lincsum  39815  lincscm  39816  lindslinindimp2lem4  39847  lindslinindsimp2lem5  39848  lincresunit3lem2  39866  aacllem  40133