Theorem mpteq2dva 4476

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1370   e. wcel 1758   |-> cmpt 4448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-ral 2800  df-opab 4449  df-mpt 4450

This theorem is referenced by:  mpteq2dv  4477  fmptapd  6001  offval  6427  offval2  6436  caofinvl  6447  caofcom  6452  caofass  6454  caofdi  6456  caofdir  6457  caonncan  6458  curry1  6764  curry2  6767  mpt2curryd  6888  pw2f1olem  7515  mapxpen  7577  xpmapenlem  7578  cantnfp1  7990  cantnflem1d  7997  cantnflem1  7998  cantnfp1OLD  8016  cantnflem1dOLD  8020  cantnflem1OLD  8021  cnfcom2lem  8035  cnfcom2lemOLD  8043  dfac12lem1  8413  seqof  11964  seqof2  11965  swrd0val  12419  swrdswrd  12456  repswswrd  12524  repswrevw  12526  revco  12564  ccatco  12565  repsco  12569  lo1eq  13148  rlimeq  13149  lo1mul2  13208  o1dif  13209  lo1sub  13210  rlimdiv  13225  caucvgr  13255  sumeq1  13268  fsumrlim  13376  fsumo1  13377  climfsum  13385  geomulcvg  13438  vdwlem8  14151  restid2  14471  pwsplusgval  14530  pwsmulrval  14531  pwsvscafval  14534  divsin  14584  xpsaddlem  14615  xpsvsca  14619  catidd  14720  fuclid  14978  fucrid  14979  fucass  14980  setcepi  15058  prf1st  15116  prf2nd  15117  1st2ndprf  15118  curfcl  15144  curfuncf  15150  diag2  15157  curf2ndf  15159  hof2val  15168  hofcllem  15170  hofcl  15171  yonedalem4a  15187  yonedalem4c  15189  yonedalem3b  15191  yonedainv  15193  yonffthlem  15194  prdsidlem  15555  prdsmndd  15556  pwsco2mhm  15601  frmdup3  15646  grpinvpropd  15703  prdsinvlem  15765  pwsinvg  15769  pwssub  15770  galactghm  16010  cayleylem1  16019  pmtrprfval  16095  sylow1lem2  16202  sylow3lem1  16230  efginvrel1  16329  frgpup3lem  16378  frgpup3  16379  prdscmnd  16447  iscyggen  16461  gsumval3OLD  16486  gsumval3  16489  gsumcllem  16490  gsumcllemOLD  16491  gsumzsplit  16522  gsumzsplitOLD  16523  gsummptshft  16534  gsumsub  16552  gsumsubOLD  16553  gsumsnd  16555  gsum2d  16568  gsum2dOLD  16569  gsum2d2  16571  gsumxp  16573  gsumxpOLD  16575  prdsgsum  16576  prdsgsumOLD  16577  dprdfsub  16616  dprdfeq0  16617  dprdfsubOLD  16623  dprdfeq0OLD  16624  dprddisj2  16642  dprddisj2OLD  16643  dprd2d2  16648  dpjidcl  16662  dpjidclOLD  16669  ablfaclem2  16692  ablfac2  16695  srgbinomlem3  16746  srgbinomlem4  16747  srgbinomlem  16748  gsumdixpOLD  16806  gsumdixp  16807  prdsmgp  16808  prdsrngd  16810  prdslmodd  17156  asclpropd  17522  psrass1lem  17553  psrlinv  17574  psrass1  17584  psrdi  17585  psrdir  17586  psrass23l  17587  psrcom  17588  psrass23  17589  resspsrmul  17596  mplsubrglem  17624  mplsubrglemOLD  17625  mplmonmul  17650  mplcoe1  17651  mplcoe5  17655  mplcoe2OLD  17657  mplcoe4  17692  evlslem3  17707  evlslem1  17708  psrplusgpropd  17797  psropprmul  17800  coe1mul2  17830  coe1tm  17834  coe1tmmul2  17837  coe1tmmul  17838  coe1pwmul  17840  ply1coe  17855  ply1coeOLD  17856  evl1gsummon  17908  mulgrhm2  18036  mulgrhm2OLD  18039  frgpcyg  18115  evpmodpmf1o  18135  phlpropd  18193  frlmphl  18315  uvcresum  18327  frlmup1  18335  mamures  18399  grpvrinv  18405  mhmvlin  18406  mamuass  18415  mamudi  18416  mamudir  18417  mamuvs1  18418  mamuvs2  18419  mamutpos  18454  madetsumid  18457  1mavmul  18470  mavmulass  18471  mvmumamul1  18476  mulmarep1gsum1  18495  mulmarep1gsum2  18496  mdetleib2  18510  mdetfval1  18512  mdet0pr  18514  mdetdiag  18521  mdetdiagid  18522  mdetrlin  18524  mdetrsca  18525  mdetralt  18530  mdetunilem9  18542  gsummatr01  18581  smadiadetlem1a  18585  smadiadetlem3  18590  smadiadetlem4  18591  neiptopnei  18852  neiptopreu  18853  ptcnplem  19310  cnmpt1t  19354  cnmpt12  19356  cnmptkp  19369  cnmptk1  19370  cnmpt1k  19371  cnmptkk  19372  cnmptk1p  19374  cnmpt2k  19377  qtopeu  19405  pt1hmeo  19495  ptunhmeo  19497  xkocnv  19503  xkohmeo  19504  flfcnp2  19696  cnmpt1plusg  19774  istgp2  19778  tmdmulg  19779  tgpmulg  19780  tmdgsum  19782  symgtgp  19788  subgtgp  19792  tgpconcomp  19799  prdstgpd  19811  tsmsmhm  19836  tsmsadd  19837  tsmssub  19839  tgptsmscls  19840  tsmssplit  19842  tsmsxplem1  19843  tsmsxplem2  19844  cnmpt1vsca  19884  tlmtgp  19886  ustuqtoplem  19930  utopsnneip  19939  ressprdsds  20062  metuvalOLD  20240  metuval  20241  nmfval2  20299  tngnm  20353  nmoeq0  20431  idnghm  20438  cnmpt1ds  20535  fsumcn  20562  expcn  20564  divccn  20565  divccncf  20598  negcncf  20610  copco  20706  pcopt  20710  pcopt2  20711  pcoass  20712  pi1xfrcnvlem  20744  cnmpt1ip  20875  rrxnm  21011  rrxds  21013  minveclem3b  21031  ovolctb  21089  ovoliunnul  21106  voliunlem3  21149  ovolfs2  21167  uniioombllem2  21179  vitalilem4  21207  vitalilem5  21208  ismbf  21224  mbfss  21240  mbfmulc2re  21242  mbfneg  21244  mbfpos  21245  mbfposb  21247  mbfadd  21255  mbfsub  21256  mbfmulc2  21257  mbfinf  21259  mbflimsup  21260  mbflimlem  21261  i1fpos  21300  i1fposd  21301  itg1climres  21308  mbfmul  21320  itg2mulc  21341  itg2i1fseq  21349  itg2cnlem1  21355  itg2cnlem2  21356  itgresr  21372  iblneg  21396  i1fibl  21401  itgitg1  21402  iblsub  21415  itgfsum  21420  itgmulc2lem1  21425  limcmpt  21474  limccnp  21482  limcco  21484  dvreslem  21500  dvres2lem  21501  dvidlem  21506  dvcnp2  21510  dvaddbr  21528  dvmulbr  21529  dvmulf  21533  dvcmulf  21535  dvcobr  21536  dvcof  21538  dvcjbr  21539  dvcj  21540  dvfre  21541  dvexp  21543  dvexp2  21544  dvrec  21545  dvmptcmul  21554  dvmptdivc  21555  dvmptneg  21556  dvmptsub  21557  dvmptre  21559  dvmptim  21560  dvmptfsum  21563  dvcnvlem  21564  dvcnv  21565  dvexp3  21566  dvef  21568  dvsincos  21569  dv11cn  21589  lhop2  21603  lhop  21604  ftc2  21632  itgparts  21635  itgsubstlem  21636  mdegfval  21647  mdegmullem  21665  ply1termlem  21787  plypow  21789  plyconst  21790  plyeq0lem  21794  plypf1  21796  plyaddlem1  21797  plymullem1  21798  coeeulem  21808  coeidlem  21821  plyco  21825  coeeq2  21826  0dgr  21829  0dgrb  21830  dgrcolem1  21856  dgrcolem2  21857  plycjlem  21859  dvply1  21866  dvply2g  21867  plydiveu  21880  plyremlem  21886  elqaalem3  21903  taylfval  21940  dvtaylp  21951  taylthlem1  21954  taylthlem2  21955  ulmshft  21971  mtestbdd  21986  iblulm  21988  itgulm2  21990  pserulm  22003  psercn2  22004  pserdvlem2  22009  pserdv  22010  pserdv2  22011  abelthlem1  22012  abelthlem3  22014  advlog  22215  advlogexp  22216  dvcxp1  22296  dvcxp2  22297  sqrcn  22304  loglesqr  22312  dvatan  22446  atantayl2  22449  atantayl3  22450  leibpi  22453  rlimcnp2  22476  efrlim  22479  dfef2  22480  cxp2lim  22486  divsqrsumlem  22489  ftalem7  22532  basellem9  22542  muinv  22649  logfacrlim  22679  logexprlim  22680  dchrmulid2  22707  dchrinvcl  22708  lgseisenlem3  22806  lgseisenlem4  22807  chtppilimlem2  22839  chebbnd2  22842  chpchtlim  22844  chpo1ub  22845  rpvmasumlem  22852  dchrmusumlema  22858  dchrvmasumlem1  22860  dchrvmasumiflem2  22867  dchrisum0fno1  22876  rpvmasum2  22877  dchrisum0lema  22879  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrisum0  22885  dchrmusumlem  22887  dchrvmasumlem  22888  rpvmasum  22891  rplogsum  22892  logdivsum  22898  mulog2sumlem3  22901  vmalogdivsum2  22903  vmalogdivsum  22904  2vmadivsumlem  22905  logsqvma2  22908  log2sumbnd  22909  selberglem2  22911  selberg3lem1  22922  selberg3  22924  selberg4lem1  22925  selberg4  22926  pntrsumo1  22930  selberg3r  22934  selberg4r  22935  selberg34r  22936  pntrlog2bndlem2  22943  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  padicabvf  22996  padicabvcxp  22997  mirval  23185  chscllem4  25178  brafnmul  25490  kbmul  25494  ofresid  26094  ofoprabco  26116  fcobijfs  26160  gsumsn2  26377  gsummptf1o  26381  xrge0mulc1cn  26505  esumval  26634  esumsn  26649  esumpcvgval  26661  esumcvg  26669  ofcfeqd2  26677  meascnbl  26767  sitgval  26852  probmeasb  26947  cndprobprob  26955  dstfrvclim1  26994  ballotlemfval  27006  ballotlemsval  27025  ballotlemieq  27033  ofccat  27075  plymul02  27081  plymulx0  27082  plymulx  27083  signsplypnf  27085  signstfv  27098  signstfvn  27104  signstfvp  27106  lgamgulmlem2  27150  lgamgulm2  27156  lgamcvglem  27160  gamcvg2lem  27179  ptpcon  27256  cvmliftlem6  27313  cvmliftphtlem  27340  cvmlift3lem5  27346  divcnvlin  27533  ovoliunnfl  28571  voliunnfl  28573  volsupnfl  28574  mbfposadd  28577  itg2addnclem  28581  itg2addnclem3  28583  itg2addnc  28584  itgaddnclem2  28589  itgaddnc  28590  iblsubnc  28591  itgsubnc  28592  itgmulc2nclem1  28596  itgmulc2nclem2  28597  itgmulc2nc  28598  itgabsnc  28599  ftc1cnnclem  28603  ftc1anclem3  28607  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem8  28612  ftc1anc  28613  ftc2nc  28614  dvcncxp1  28615  areacirclem1  28622  areacirclem2  28623  areacirclem4  28625  areacirc  28627  upixp  28761  mzpsubst  29223  mzprename  29224  mzpcompact2lem  29226  eldioph2  29238  rabdiophlem2  29278  mendlmod  29688  mendassa  29689  areaquad  29730  expgrowthi  29745  expgrowth  29747  mulc1cncfg  29908  expcnfg  29911  clim1fr1  29912  ibliccsinexp  29929  itgsinexplem1  29932  itgsinexp  29933  stoweidlem4  29937  stirlinglem5  30011  wwlknprop  30458  fdmdifeqresdif  30870  telescfzgsumis  30952  telescfzgsum0is  30954  eqcoe1ply1eq  30977  ply1mulgsumlem2  30987  cply1mul  30993  lply1binomsc  30998  mpt2matmul  31016  dmatmul  31030  lincvalsc0  31062  linc0scn0  31064  lincdifsn  31065  lincsum  31070  lincscm  31071  lindslinindimp2lem4  31102  lindslinindsimp2lem5  31103  lincresunit3lem2  31121  cpmatmcllem  31181  mat2pmatmul  31194  m2cpminv  31222  pmatcollpw1dstlem1  31227  pmatcollpw1dst  31228  pmatcollpw1lem4  31230  pmatcollpw1lem5  31231  pmatcollpw3  31238  pmatcollpw4  31240  pmatcollpw4fi  31241  pmatcollpwscmat  31248  idpmattoidmply1  31260  mp2pm2mplem3  31263  mp2pm2mplem4  31264  mp2pm2mplem5  31265  mp2pm2mp  31266  pmattomply1ghm  31270  pmattomply1mhmlem2  31274  monmat2matmon  31278  pmat2matp  31279  cpdmat  31295  cpscmat  31296  cpscmatgsumbin  31298  cpscmatgsummon  31299  cp0mat  31300  cpidmat  31301  chfacfscmulgsum  31314  chfacfpmmulgsum  31318  chfacfpmmulgsum2  31319  cayhamlem1  31320  cpmidgsumm2pm  31323  cpmidpmat  31327  cpmadugsumlemB  31328  cpmadugsumlemC  31329  cpmadugsumlemF  31330  cpmadumatpoly  31338  cayhamlem3  31342  cayhamlem4  31343  cayleyhamilton0  31344  cayleyhamiltonALT  31346  bj-finsumval0  32889