Theorem mpteq2dva 4453

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

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1399   e. wcel 1826   |-> cmpt 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-ral 2737  df-opab 4426  df-mpt 4427

This theorem is referenced by:  mpteq2dv  4454  2fvcoidd  6101  offval  6446  offval2  6455  caofinvl  6466  caofcom  6471  caofass  6473  caofdi  6475  caofdir  6476  caonncan  6477  curry1  6791  curry2  6794  mpt2curryd  6916  pw2f1olem  7540  mapxpen  7602  xpmapenlem  7603  cantnfp1  8013  cantnflem1d  8020  cantnflem1  8021  cantnfp1OLD  8039  cantnflem1dOLD  8043  cantnflem1OLD  8044  cnfcom2lem  8058  cnfcom2lemOLD  8066  dfac12lem1  8436  seqof  12067  seqof2  12068  swrd0val  12557  swrdswrd  12596  repswswrd  12667  repswrevw  12669  revco  12711  ccatco  12712  repsco  12716  lo1eq  13393  rlimeq  13394  lo1mul2  13453  o1dif  13454  lo1sub  13455  rlimdiv  13470  caucvgr  13500  sumeq1  13513  fsumrlim  13627  fsumo1  13628  climfsum  13636  geomulcvg  13687  vdwlem8  14508  restid2  14838  pwsplusgval  14897  pwsmulrval  14898  pwsvscafval  14901  qusin  14951  xpsaddlem  14982  xpsvsca  14986  catidd  15087  fuclid  15372  fucrid  15373  fucass  15374  setcepi  15484  prf1st  15590  prf2nd  15591  1st2ndprf  15592  curfcl  15618  curfuncf  15624  diag2  15631  curf2ndf  15633  hof2val  15642  hofcllem  15644  hofcl  15645  yonedalem4a  15661  yonedalem4c  15663  yonedalem3b  15665  yonedainv  15667  yonffthlem  15668  prdsidlem  16069  prdsmndd  16070  pwsco2mhm  16119  frmdup3lem  16151  frmdup3  16152  grpinvpropd  16230  prdsinvlem  16295  pwsinvg  16299  pwssub  16300  galactghm  16545  cayleylem1  16554  pmtrprfval  16629  sylow1lem2  16736  sylow3lem1  16764  efginvrel1  16863  frgpup3lem  16912  frgpup3  16913  prdscmnd  16984  iscyggen  17000  gsumval3OLD  17025  gsumval3  17028  gsumcllem  17029  gsumcllemOLD  17030  gsumzsplit  17061  gsumzsplitOLD  17062  gsumsub  17089  gsummptf1o  17104  gsum2d  17113  gsum2dOLD  17114  gsum2d2  17116  gsumxp  17118  prdsgsum  17120  prdsgsumOLD  17121  telgsumfz  17132  telgsumfz0  17134  telgsum  17136  dprdfsub  17174  dprdfeq0  17175  dprdfsubOLD  17181  dprdfeq0OLD  17182  dprddisj2  17200  dprddisj2OLD  17201  dprd2d2  17206  dpjidcl  17220  dpjidclOLD  17227  ablfaclem2  17250  ablfac2  17253  srgbinomlem3  17306  srgbinomlem4  17307  srgbinomlem  17308  gsumdixpOLD  17370  gsumdixp  17371  prdsmgp  17372  prdsringd  17374  prdslmodd  17728  asclpropd  18108  psrass1lem  18142  psrlinv  18163  psrass1  18173  psrdi  18174  psrdir  18175  psrass23l  18176  psrcom  18177  psrass23  18178  resspsrmul  18185  mplsubrglem  18213  mplsubrglemOLD  18214  mplmonmul  18239  mplcoe1  18240  mplcoe5  18244  mplcoe2OLD  18246  mplcoe4  18281  evlslem3  18296  evlslem1  18297  psrplusgpropd  18390  psropprmul  18392  coe1mul2  18423  coe1tm  18427  coe1tmmul2  18430  coe1tmmul  18431  coe1pwmul  18433  cply1mul  18448  ply1coe  18450  ply1coeOLD  18451  eqcoe1ply1eq  18452  lply1binomsc  18462  evl1gsummon  18514  mulgrhm2  18629  frgpcyg  18703  evpmodpmf1o  18723  phlpropd  18781  frlmphl  18901  uvcresum  18913  frlmup1  18918  mamures  18977  grpvrinv  18983  mhmvlin  18984  mamuass  18989  mamudi  18990  mamudir  18991  mamuvs1  18992  mamuvs2  18993  mpt2matmul  19033  mamutpos  19045  madetsumid  19048  dmatmul  19084  scmatscm  19100  1mavmul  19135  mavmulass  19136  mvmumamul1  19141  mulmarep1gsum1  19160  mulmarep1gsum2  19161  mdetleib2  19175  mdetfval1  19177  mdet0pr  19179  mdetdiag  19186  mdetdiagid  19187  mdetrlin  19189  mdetrsca  19190  mdetralt  19195  mdetunilem9  19207  gsummatr01  19246  smadiadetlem1a  19250  smadiadetlem3  19255  smadiadetlem4  19256  cpmatmcllem  19304  mat2pmatmul  19317  decpmatmullem  19357  decpmatmul  19358  pmatcollpw1lem2  19361  pmatcollpw  19367  pmatcollpw3lem  19369  pmatcollpwscmat  19377  idpm2idmp  19387  mp2pm2mplem3  19394  mp2pm2mplem4  19395  mp2pm2mplem5  19396  mp2pm2mp  19397  pm2mpghm  19402  pm2mpmhmlem2  19405  monmat2matmon  19410  pm2mp  19411  chpdmat  19427  chpscmat  19428  chpscmatgsumbin  19430  chpscmatgsummon  19431  chp0mat  19432  chpidmat  19433  chfacfscmulgsum  19446  chfacfpmmulgsum  19450  chfacfpmmulgsum2  19451  cayhamlem1  19452  cpmidgsumm2pm  19455  cpmidpmat  19459  cpmadugsumlemB  19460  cpmadugsumlemC  19461  cpmadugsumlemF  19462  cpmadumatpoly  19469  cayhamlem3  19473  cayhamlem4  19474  cayleyhamilton0  19475  cayleyhamiltonALT  19477  neiptopnei  19719  neiptopreu  19720  ptcnplem  20207  cnmpt1t  20251  cnmpt12  20253  cnmptkp  20266  cnmptk1  20267  cnmpt1k  20268  cnmptkk  20269  cnmptk1p  20271  cnmpt2k  20274  qtopeu  20302  pt1hmeo  20392  ptunhmeo  20394  xkocnv  20400  xkohmeo  20401  flfcnp2  20593  cnmpt1plusg  20671  istgp2  20675  tmdmulg  20676  tgpmulg  20677  tmdgsum  20679  symgtgp  20685  subgtgp  20689  tgpconcomp  20696  prdstgpd  20708  tsmsmhm  20733  tsmsadd  20734  tsmssub  20736  tgptsmscls  20737  tsmssplit  20739  tsmsxplem1  20740  tsmsxplem2  20741  cnmpt1vsca  20781  tlmtgp  20783  ustuqtoplem  20827  utopsnneip  20836  ressprdsds  20959  metuvalOLD  21137  metuval  21138  nmfval2  21196  tngnm  21250  nmoeq0  21328  idnghm  21335  cnmpt1ds  21432  fsumcn  21459  expcn  21461  divccn  21462  divccncf  21495  negcncf  21507  copco  21603  pcopt  21607  pcopt2  21608  pcoass  21609  pi1xfrcnvlem  21641  cnmpt1ip  21772  rrxnm  21908  rrxds  21910  minveclem3b  21928  ovolctb  21986  ovoliunnul  22003  voliunlem3  22047  ovolfs2  22065  uniioombllem2  22077  vitalilem4  22105  vitalilem5  22106  ismbf  22122  mbfss  22138  mbfmulc2re  22140  mbfneg  22142  mbfpos  22143  mbfposb  22145  mbfadd  22153  mbfsub  22154  mbfmulc2  22155  mbfinf  22157  mbflimsup  22158  mbflimlem  22159  i1fpos  22198  i1fposd  22199  itg1climres  22206  mbfmul  22218  itg2mulc  22239  itg2i1fseq  22247  itg2cnlem1  22253  itg2cnlem2  22254  itgresr  22270  iblneg  22294  i1fibl  22299  itgitg1  22300  iblsub  22313  itgfsum  22318  itgmulc2lem1  22323  limcmpt  22372  limccnp  22380  limcco  22382  dvreslem  22398  dvres2lem  22399  dvidlem  22404  dvcnp2  22408  dvaddbr  22426  dvmulbr  22427  dvmulf  22431  dvcmulf  22433  dvcobr  22434  dvcof  22436  dvcjbr  22437  dvcj  22438  dvfre  22439  dvexp  22441  dvexp2  22442  dvrec  22443  dvmptcmul  22452  dvmptdivc  22453  dvmptneg  22454  dvmptsub  22455  dvmptre  22457  dvmptim  22458  dvmptfsum  22461  dvcnvlem  22462  dvcnv  22463  dvexp3  22464  dvef  22466  dvsincos  22467  dv11cn  22487  lhop2  22501  lhop  22502  ftc2  22530  itgparts  22533  itgsubstlem  22534  mdegfval  22545  mdegmullem  22563  ply1termlem  22685  plypow  22687  plyconst  22688  plyeq0lem  22692  plypf1  22694  plyaddlem1  22695  plymullem1  22696  coeeulem  22706  coeidlem  22719  plyco  22723  coeeq2  22724  0dgr  22727  0dgrb  22728  dgrcolem1  22755  dgrcolem2  22756  plycjlem  22758  dvply1  22765  dvply2g  22766  plydiveu  22779  plyremlem  22785  elqaalem3  22802  taylfval  22839  dvtaylp  22850  taylthlem1  22853  taylthlem2  22854  ulmshft  22870  mtestbdd  22885  iblulm  22887  itgulm2  22889  pserulm  22902  psercn2  22903  pserdvlem2  22908  pserdv  22909  pserdv2  22910  abelthlem1  22911  abelthlem3  22913  advlog  23122  advlogexp  23123  dvcxp1  23203  dvcxp2  23204  sqrtcn  23211  loglesqrt  23219  dvatan  23382  atantayl2  23385  atantayl3  23386  leibpi  23389  rlimcnp2  23413  efrlim  23416  dfef2  23417  cxp2lim  23423  divsqrtsumlem  23426  ftalem7  23469  basellem9  23479  muinv  23586  logfacrlim  23616  logexprlim  23617  dchrmulid2  23644  dchrinvcl  23645  lgseisenlem3  23743  lgseisenlem4  23744  chtppilimlem2  23776  chebbnd2  23779  chpchtlim  23781  chpo1ub  23782  rpvmasumlem  23789  dchrmusumlema  23795  dchrvmasumlem1  23797  dchrvmasumiflem2  23804  dchrisum0fno1  23813  rpvmasum2  23814  dchrisum0lema  23816  dchrisum0lem1  23818  dchrisum0lem2a  23819  dchrisum0lem2  23820  dchrisum0  23822  dchrmusumlem  23824  dchrvmasumlem  23825  rpvmasum  23828  rplogsum  23829  logdivsum  23835  mulog2sumlem3  23838  vmalogdivsum2  23840  vmalogdivsum  23841  2vmadivsumlem  23842  logsqvma2  23845  log2sumbnd  23846  selberglem2  23848  selberg3lem1  23859  selberg3  23861  selberg4lem1  23862  selberg4  23863  pntrsumo1  23867  selberg3r  23871  selberg4r  23872  selberg34r  23873  pntrlog2bndlem2  23880  pntrlog2bndlem4  23882  pntrlog2bndlem5  23883  pntrlog2bndlem6  23885  padicabvf  23933  padicabvcxp  23934  mirval  24156  wwlknprop  24807  chscllem4  26675  brafnmul  26986  kbmul  26990  ofresid  27622  ofoprabco  27651  fcobijfs  27699  gsummpt2d  27925  xrge0mulc1cn  28077  esumval  28194  esumsnf  28212  esumpcvgval  28226  esumcvg  28234  esumcvgsum  28236  esumsup  28237  ofcfeqd2  28249  meascnbl  28346  sitgval  28457  probmeasb  28552  cndprobprob  28560  dstfrvclim1  28599  ballotlemfval  28611  ballotlemsval  28630  ballotlemieq  28638  ofccat  28680  plymul02  28686  plymulx0  28687  plymulx  28688  signsplypnf  28690  signstfv  28703  signstfvn  28709  signstfvp  28711  lgamgulmlem2  28761  lgamgulm2  28767  lgamcvglem  28771  gamcvg2lem  28790  ptpcon  28867  cvmliftlem6  28924  cvmliftphtlem  28951  cvmlift3lem5  28957  elmrsubrn  29069  msubfval  29073  msubco  29080  divcnvlin  29284  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  mbfposadd  30227  itg2addnclem  30232  itg2addnclem3  30234  itg2addnc  30235  itgaddnclem2  30240  itgaddnc  30241  iblsubnc  30242  itgsubnc  30243  itgmulc2nclem1  30247  itgmulc2nclem2  30248  itgmulc2nc  30249  itgabsnc  30250  ftc1cnnclem  30254  ftc1anclem3  30258  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anclem8  30263  ftc1anc  30264  ftc2nc  30265  dvcncxp1  30266  areacirclem1  30273  areacirclem2  30274  areacirclem4  30276  areacirc  30278  upixp  30386  mzpsubst  30846  mzprename  30847  mzpcompact2lem  30849  eldioph2  30860  rabdiophlem2  30901  mendlmod  31310  mendassa  31311  areaquad  31352  hashnzfzclim  31395  expgrowthi  31406  expgrowth  31408  uzmptshftfval  31419  dvradcnv2  31420  binomcxplemrat  31423  binomcxplemfrat  31424  binomcxplemradcnv  31425  binomcxplemdvbinom  31426  binomcxplemcvg  31427  binomcxplemdvsum  31428  binomcxplemnotnn0  31429  mulc1cncfg  31749  expcnfg  31752  clim1fr1  31773  divcnvg  31799  sublimc  31824  reclimc  31825  divlimc  31828  cncfmptssg  31838  negcncfg  31849  divcncf  31852  cncficcgt0  31857  fprodcncf  31870  dvrecg  31873  dvsinax  31874  dvmptdiv  31880  dvasinbx  31883  dvdivf  31885  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvnmptdivc  31901  dvxpaek  31903  dvnxpaek  31905  dvnmul  31906  dvnprodlem2  31910  ibliccsinexp  31915  itgsinexplem1  31918  itgsinexp  31919  iblempty  31930  itgcoscmulx  31934  itgsincmulx  31939  itgioocnicc  31942  iblcncfioo  31943  itgsbtaddcnst  31947  stoweidlem4  31952  stirlinglem5  32026  dirkerval  32039  dirkertrigeq  32049  dirkeritg  32050  dirkercncflem2  32052  dirkercncflem4  32054  fourierdlem16  32071  fourierdlem18  32073  fourierdlem21  32076  fourierdlem22  32077  fourierdlem28  32083  fourierdlem39  32094  fourierdlem40  32095  fourierdlem41  32096  fourierdlem53  32108  fourierdlem56  32111  fourierdlem57  32112  fourierdlem60  32115  fourierdlem61  32116  fourierdlem68  32123  fourierdlem73  32128  fourierdlem74  32129  fourierdlem75  32130  fourierdlem76  32131  fourierdlem78  32133  fourierdlem81  32136  fourierdlem82  32137  fourierdlem83  32138  fourierdlem84  32139  fourierdlem85  32140  fourierdlem88  32143  fourierdlem90  32145  fourierdlem92  32147  fourierdlem93  32148  fourierdlem95  32150  fourierdlem97  32152  fourierdlem101  32156  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  fourierdlem112  32167  sqwvfoura  32177  sqwvfourb  32178  fouriersw  32180  elaa2lem  32182  etransclem4  32187  etransclem17  32200  etransclem18  32201  etransclem32  32215  etransclem46  32229  fdmdifeqresdif  33131  ply1mulgsumlem2  33187  lincvalsc0  33222  linc0scn0  33224  lincdifsn  33225  lincsum  33230  lincscm  33231  lindslinindimp2lem4  33262  lindslinindsimp2lem5  33263  lincresunit3lem2  33281  aacllem  33550  bj-finsumval0  35010