Theorem mpteq2dva 4373

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   e. cmpt 4345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2715  df-opab 4346  df-mpt 4347

This theorem is referenced by:  mpteq2dv  4374  fmptapd  5897  offval  6322  offval2  6331  caofinvl  6342  caofcom  6347  caofass  6349  caofdi  6351  caofdir  6352  caonncan  6353  curry1  6659  curry2  6662  pw2f1olem  7407  mapxpen  7469  xpmapenlem  7470  cantnfp1  7881  cantnflem1d  7888  cantnflem1  7889  cantnfp1OLD  7907  cantnflem1dOLD  7911  cantnflem1OLD  7912  cnfcom2lem  7926  cnfcom2lemOLD  7934  dfac12lem1  8304  seqof  11855  seqof2  11856  swrd0val  12309  swrdswrd  12346  repswswrd  12414  repswrevw  12416  revco  12454  ccatco  12455  repsco  12459  lo1eq  13038  rlimeq  13039  lo1mul2  13098  o1dif  13099  lo1sub  13100  rlimdiv  13115  caucvgr  13145  sumeq1  13158  fsumrlim  13266  fsumo1  13267  climfsum  13275  geomulcvg  13328  vdwlem8  14041  restid2  14361  pwsplusgval  14420  pwsmulrval  14421  pwsvscafval  14424  divsin  14474  xpsaddlem  14505  xpsvsca  14509  catidd  14610  fuclid  14868  fucrid  14869  fucass  14870  setcepi  14948  prf1st  15006  prf2nd  15007  1st2ndprf  15008  curfcl  15034  curfuncf  15040  diag2  15047  curf2ndf  15049  hof2val  15058  hofcllem  15060  hofcl  15061  yonedalem4a  15077  yonedalem4c  15079  yonedalem3b  15081  yonedainv  15083  yonffthlem  15084  prdsidlem  15445  prdsmndd  15446  pwsco2mhm  15490  frmdup3  15535  grpinvpropd  15592  prdsinvlem  15654  pwsinvg  15658  pwssub  15659  galactghm  15899  cayleylem1  15908  pmtrprfval  15984  sylow1lem2  16089  sylow3lem1  16117  efginvrel1  16216  frgpup3lem  16265  frgpup3  16266  prdscmnd  16334  iscyggen  16348  gsumval3OLD  16373  gsumval3  16376  gsumcllem  16377  gsumcllemOLD  16378  gsumzsplit  16409  gsumzsplitOLD  16410  gsummptshft  16419  gsumsub  16437  gsumsubOLD  16438  gsumsnd  16440  gsum2d  16451  gsum2dOLD  16452  gsum2d2  16454  gsumxp  16456  gsumxpOLD  16458  prdsgsum  16459  prdsgsumOLD  16460  dprdfsub  16499  dprdfeq0  16500  dprdfsubOLD  16506  dprdfeq0OLD  16507  dprddisj2  16525  dprddisj2OLD  16526  dprd2d2  16531  dpjidcl  16545  dpjidclOLD  16552  ablfaclem2  16575  ablfac2  16578  srgbinomlem3  16628  srgbinomlem4  16629  srgbinomlem  16630  gsumdixpOLD  16688  gsumdixp  16689  prdsmgp  16690  prdsrngd  16692  prdslmodd  17027  asclpropd  17393  psrass1lem  17424  psrlinv  17445  psrass1  17455  psrdi  17456  psrdir  17457  psrcom  17458  psrass23  17459  resspsrmul  17466  mplsubrglem  17494  mplsubrglemOLD  17495  mplmonmul  17520  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  mplcoe4  17560  evlslem3  17575  evlslem1  17576  psrplusgpropd  17665  psropprmul  17668  coe1mul2  17698  coe1tm  17701  coe1tmmul2  17704  coe1tmmul  17705  coe1pwmul  17707  ply1coe  17721  ply1coeOLD  17722  evl1gsummon  17774  mulgrhm2  17902  mulgrhm2OLD  17905  frgpcyg  17981  evpmodpmf1o  18001  phlpropd  18059  frlmphl  18181  uvcresum  18193  frlmup1  18201  mamures  18265  grpvrinv  18271  mhmvlin  18272  mamuass  18281  mamudi  18282  mamudir  18283  mamuvs1  18284  mamuvs2  18285  mamutpos  18318  madetsumid  18321  1mavmul  18334  mavmulass  18335  mvmumamul1  18340  mulmarep1gsum1  18359  mulmarep1gsum2  18360  mdetleib2  18374  mdetfval1  18376  mdet0pr  18378  mdet1  18383  mdetrlin  18384  mdetrsca  18385  mdetralt  18389  mdetunilem9  18401  gsummatr01  18440  smadiadetlem1a  18444  smadiadetlem3  18449  smadiadetlem4  18450  neiptopnei  18711  neiptopreu  18712  ptcnplem  19169  cnmpt1t  19213  cnmpt12  19215  cnmptkp  19228  cnmptk1  19229  cnmpt1k  19230  cnmptkk  19231  cnmptk1p  19233  cnmpt2k  19236  qtopeu  19264  pt1hmeo  19354  ptunhmeo  19356  xkocnv  19362  xkohmeo  19363  flfcnp2  19555  cnmpt1plusg  19633  istgp2  19637  tmdmulg  19638  tgpmulg  19639  tmdgsum  19641  symgtgp  19647  subgtgp  19651  tgpconcomp  19658  prdstgpd  19670  tsmsmhm  19695  tsmsadd  19696  tsmssub  19698  tgptsmscls  19699  tsmssplit  19701  tsmsxplem1  19702  tsmsxplem2  19703  cnmpt1vsca  19743  tlmtgp  19745  ustuqtoplem  19789  utopsnneip  19798  ressprdsds  19921  metuvalOLD  20099  metuval  20100  nmfval2  20158  tngnm  20212  nmoeq0  20290  idnghm  20297  cnmpt1ds  20394  fsumcn  20421  expcn  20423  divccn  20424  divccncf  20457  negcncf  20469  copco  20565  pcopt  20569  pcopt2  20570  pcoass  20571  pi1xfrcnvlem  20603  cnmpt1ip  20734  rrxnm  20870  rrxds  20872  minveclem3b  20890  ovolctb  20948  ovoliunnul  20965  voliunlem3  21008  ovolfs2  21026  uniioombllem2  21038  vitalilem4  21066  vitalilem5  21067  ismbf  21083  mbfss  21099  mbfmulc2re  21101  mbfneg  21103  mbfpos  21104  mbfposb  21106  mbfadd  21114  mbfsub  21115  mbfmulc2  21116  mbfinf  21118  mbflimsup  21119  mbflimlem  21120  i1fpos  21159  i1fposd  21160  itg1climres  21167  mbfmul  21179  itg2mulc  21200  itg2i1fseq  21208  itg2cnlem1  21214  itg2cnlem2  21215  itgresr  21231  iblneg  21255  i1fibl  21260  itgitg1  21261  iblsub  21274  itgfsum  21279  itgmulc2lem1  21284  limcmpt  21333  limccnp  21341  limcco  21343  dvreslem  21359  dvres2lem  21360  dvidlem  21365  dvcnp2  21369  dvaddbr  21387  dvmulbr  21388  dvmulf  21392  dvcmulf  21394  dvcobr  21395  dvcof  21397  dvcjbr  21398  dvcj  21399  dvfre  21400  dvexp  21402  dvexp2  21403  dvrec  21404  dvmptcmul  21413  dvmptdivc  21414  dvmptneg  21415  dvmptsub  21416  dvmptre  21418  dvmptim  21419  dvmptfsum  21422  dvcnvlem  21423  dvcnv  21424  dvexp3  21425  dvef  21427  dvsincos  21428  dv11cn  21448  lhop2  21462  lhop  21463  ftc2  21491  itgparts  21494  itgsubstlem  21495  mdegfval  21506  mdegmullem  21524  ply1termlem  21646  plypow  21648  plyconst  21649  plyeq0lem  21653  plypf1  21655  plyaddlem1  21656  plymullem1  21657  coeeulem  21667  coeidlem  21680  plyco  21684  coeeq2  21685  0dgr  21688  0dgrb  21689  dgrcolem1  21715  dgrcolem2  21716  plycjlem  21718  dvply1  21725  dvply2g  21726  plydiveu  21739  plyremlem  21745  elqaalem3  21762  taylfval  21799  dvtaylp  21810  taylthlem1  21813  taylthlem2  21814  ulmshft  21830  mtestbdd  21845  iblulm  21847  itgulm2  21849  pserulm  21862  psercn2  21863  pserdvlem2  21868  pserdv  21869  pserdv2  21870  abelthlem1  21871  abelthlem3  21873  advlog  22074  advlogexp  22075  dvcxp1  22155  dvcxp2  22156  sqrcn  22163  loglesqr  22171  dvatan  22305  atantayl2  22308  atantayl3  22309  leibpi  22312  rlimcnp2  22335  efrlim  22338  dfef2  22339  cxp2lim  22345  divsqrsumlem  22348  ftalem7  22391  basellem9  22401  muinv  22508  logfacrlim  22538  logexprlim  22539  dchrmulid2  22566  dchrinvcl  22567  lgseisenlem3  22665  lgseisenlem4  22666  chtppilimlem2  22698  chebbnd2  22701  chpchtlim  22703  chpo1ub  22704  rpvmasumlem  22711  dchrmusumlema  22717  dchrvmasumlem1  22719  dchrvmasumiflem2  22726  dchrisum0fno1  22735  rpvmasum2  22736  dchrisum0lema  22738  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0lem2  22742  dchrisum0  22744  dchrmusumlem  22746  dchrvmasumlem  22747  rpvmasum  22750  rplogsum  22751  logdivsum  22757  mulog2sumlem3  22760  vmalogdivsum2  22762  vmalogdivsum  22763  2vmadivsumlem  22764  logsqvma2  22767  log2sumbnd  22768  selberglem2  22770  selberg3lem1  22781  selberg3  22783  selberg4lem1  22784  selberg4  22785  pntrsumo1  22789  selberg3r  22793  selberg4r  22794  selberg34r  22795  pntrlog2bndlem2  22802  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  padicabvf  22855  padicabvcxp  22856  mirval  23027  chscllem4  24994  brafnmul  25306  kbmul  25310  ofresid  25911  ofoprabco  25933  fcobijfs  25977  gsumsn2  26194  gsummptf1o  26198  xrge0mulc1cn  26323  esumval  26452  esumsn  26467  esumpcvgval  26479  esumcvg  26487  ofcfeqd2  26495  meascnbl  26585  sitgval  26670  probmeasb  26765  cndprobprob  26773  dstfrvclim1  26812  ballotlemfval  26824  ballotlemsval  26843  ballotlemieq  26851  ofccat  26893  plymul02  26899  plymulx0  26900  plymulx  26901  signsplypnf  26903  signstfv  26916  signstfvn  26922  signstfvp  26924  lgamgulmlem2  26968  lgamgulm2  26974  lgamcvglem  26978  gamcvg2lem  26997  ptpcon  27074  cvmliftlem6  27131  cvmliftphtlem  27158  cvmlift3lem5  27164  divcnvlin  27350  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  mbfposadd  28392  itg2addnclem  28396  itg2addnclem3  28398  itg2addnc  28399  itgaddnclem2  28404  itgaddnc  28405  iblsubnc  28406  itgsubnc  28407  itgmulc2nclem1  28411  itgmulc2nclem2  28412  itgmulc2nc  28413  itgabsnc  28414  ftc1cnnclem  28418  ftc1anclem3  28422  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem8  28427  ftc1anc  28428  ftc2nc  28429  dvcncxp1  28430  areacirclem1  28437  areacirclem2  28438  areacirclem4  28440  areacirc  28442  upixp  28576  mzpsubst  29038  mzprename  29039  mzpcompact2lem  29041  eldioph2  29053  rabdiophlem2  29093  mendlmod  29503  mendassa  29504  areaquad  29545  expgrowthi  29560  expgrowth  29562  mulc1cncfg  29723  expcnfg  29726  clim1fr1  29727  ibliccsinexp  29744  itgsinexplem1  29747  itgsinexp  29748  stoweidlem4  29752  stirlinglem5  29826  wwlknprop  30273  fdmdifeqresdif  30684  psrass23l  30763  lply1binomsc  30775  dmatmul  30799  pmatcollpw1lem4  30817  pmatcollpw1lem5  30818  mdetdiag  30825  mdetdiagid  30826  lincvalsc0  30844  linc0scn0  30846  lincdifsn  30847  lincsum  30852  lincscm  30853  lindslinindimp2lem4  30884  lindslinindsimp2lem5  30885  lincresunit3lem2  30903  bj-finsumval0  32426