Theorem mpteq2dv 4367

Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)

Hypothesis

Ref	Expression
mpteq2dv.1	|- ( ph -> B = C )

Assertion

Ref	Expression
mpteq2dv	|- ( 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 mpteq2dv

Step	Hyp	Ref	Expression
1		mpteq2dv.1	. . 3 |- ( ph -> B = C )
2	1	adantr 462	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	2	mpteq2dva 4366	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755   e. cmpt 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-opab 4339  df-mpt 4340

This theorem is referenced by:  ofeq  6311  rdgeq1  6853  rdgeq2  6854  omv  6940  oev  6942  oieq1  7714  oieq2  7715  cantnffvalOLD  7859  cantnflem1  7885  cantnflem1OLD  7908  wunex2  8892  wuncval2  8901  reexALT  10972  seqof2  11847  limsupval  12935  sumeq2w  13152  sumeq2ii  13153  cbvsum  13155  summo  13177  fsum  13180  fsumrlim  13256  fsumo1  13257  rpnnen2lem1  13479  rpnnen2lem2  13480  rpnnen  13491  1arithlem1  13966  vdwapval  14016  vdwlem6  14029  vdwlem8  14031  vdwlem9  14032  vdwlem10  14033  ramub1lem2  14070  ramcl  14072  prdsplusgval  14393  prdsmulrval  14395  prdsdsval  14398  prdsvscaval  14399  ismon  14654  fucco  14854  curf1  15017  curf2  15021  yonedalem4a  15067  grplactfval  15601  galactghm  15887  pmtrval  15936  sylow1  16081  sylow2b  16101  sylow3lem5  16109  sylow3  16111  iscyg  16335  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsumzmhm  16406  gsumzmhmOLD  16407  ablfac2  16563  gsumdixpOLD  16634  gsumdixp  16635  fczpsrbag  17367  psrmulfval  17389  mvrval  17427  subrgmvr  17473  mplcoe1  17477  mplcoe3  17478  mplcoe3OLD  17479  mplcoe2  17480  mplcoe2OLD  17481  mplmon2  17506  subrgascl  17511  evlslem2  17524  coe1fval  17559  zncyg  17822  phllmhm  17902  isphld  17924  frlmgsumOLD  18036  frlmgsum  18037  frlmipval  18045  frlmphl  18047  uvcval  18051  mamuval  18125  mamufv  18126  madetsumid  18187  mvmulval  18195  mvmulfv  18196  mavmulfv  18198  1mavmul  18200  marepvval0  18218  mulmarep1gsum1  18225  mdetleib  18239  mdetleib2  18240  mdetfval1  18242  mdetleib1  18243  mdet0pr  18244  mdetralt  18255  mdetunilem9  18267  m2detleib  18278  smadiadetlem3  18315  ptbasfi  18995  ptcnplem  19035  ptrescn  19053  cnmpt2k  19102  xkohmeo  19229  fmval  19357  fmf  19359  ptcmpg  19470  tmdmulg  19504  prdstmdd  19535  tsmspropd  19543  prdsxmslem2  19945  metdsval  20264  fsumcn  20287  expcn  20289  lebnumlem3  20376  pcoval  20424  pi1xfrcnv  20470  rrxds  20738  rrxmval  20745  itg11  21010  mbfi1fseqlem2  21035  mbfi1fseqlem6  21039  mbfi1fseq  21040  mbfi1flimlem  21041  mbfmullem  21044  itg2const  21059  itg2mulc  21066  itg2monolem1  21069  itg2i1fseqle  21073  itg2i1fseq  21074  itg2addlem  21077  itg2cnlem1  21080  itg2cn  21082  isibl  21084  isibl2  21085  iblitg  21087  itgz  21099  itgvallem  21103  itgvallem3  21104  iblcnlem1  21106  itgcnlem  21108  iblrelem  21109  iblposlem  21110  iblpos  21111  itgrevallem1  21113  itgposval  21114  iblss2  21124  itgss  21130  itgfsum  21145  iblabslem  21146  iblmulc2  21149  bddmulibl  21157  itgcn  21161  ellimc  21189  dvnfval  21237  cpnfval  21247  dvexp  21268  dvexp2  21269  dvmptfsum  21288  dvlipcn  21307  dvivthlem1  21321  dvfsumle  21334  dvfsumabs  21336  dvfsumlem2  21340  evlslem3  21365  evlslem1  21366  mpfrcl  21369  evlsval  21370  evlsvar  21374  mpfind  21395  pf1ind  21405  elply2  21548  elplyr  21553  elplyd  21554  coeeu  21577  coelem  21578  coeeq  21579  plyco  21593  coe11  21604  coe1termlem  21609  dgrcolem1  21624  dvply2g  21635  elqaalem3  21671  eltayl  21709  tayl0  21711  taylthlem1  21722  taylthlem2  21723  ulmcau  21744  ulmdvlem1  21749  ulmdvlem3  21751  mtest  21753  mtestbdd  21754  pserval  21759  pserulm  21771  psercn  21775  pserdvlem2  21777  abelthlem3  21782  logtayl  21989  dvcxp1  22064  dmarea  22235  musum  22415  dchrptlem2  22488  dchrptlem3  22489  dchrpt  22490  lgsval  22523  lgsval4lem  22530  lgsneg  22542  lgsmod  22544  rpvmasum2  22645  padicfval  22749  ostth2  22770  ostth3  22771  ostth  22772  htthlem  24141  htth  24142  pjhfval  24621  hosmval  24961  hommval  24962  hodmval  24963  hfsmval  24964  hfmmval  24965  brafval  25169  kbfval  25178  indval  26323  ofceq  26392  itgeq12dv  26559  ballotlemfval  26719  lgamgulmlem2  26863  lgamgulmlem5  26866  ptpcon  26969  cvmliftlem15  27034  cvmlift2lem4  27042  cvmlift2  27052  snmlval  27067  snmlflim  27068  relexp0  27177  relexpsucr  27178  prodeq2w  27271  prodmo  27295  fprod  27300  faclim  27398  faclim2  27400  trpredeq1  27530  trpredeq2  27531  bpolylem  28037  voliunnfl  28276  itg2addnclem  28284  itg2addnclem3  28286  itg2addnc  28287  itg2gt0cn  28288  iblabsnclem  28296  iblmulc2nc  28298  ftc1anclem2  28309  ftc1anclem6  28313  ftc1anclem8  28315  ftc1anc  28316  ftc2nc  28317  dvcncxp1  28318  upixp  28464  rrncmslem  28572  ismrer1  28578  mzpclval  28903  mzpcl2  28908  mzpexpmpt  28923  mzpsubst  28927  mzpcompact2lem  28930  rmxfval  29087  rmyfval  29088  aomclem8  29256  hbtlem1  29321  hbtlem7  29323  itgpowd  29432  expgrowthi  29449  expgrowth  29451  addrval  29564  subrval  29565  mulvval  29566  fmulcl  29604  fmuldfeqlem1  29605  stoweidlem2  29640  stoweidlem17  29655  stoweidlem19  29657  stoweidlem20  29658  stoweidlem43  29681  stoweidlem62  29700  stoweid  29701  wwlkn  30159  clwwlkn  30273  clwwlknprop  30278  lincop  30648  tendoplcbv  33989  tendopl  33990  tendoicbv  34007  tendoi  34008  dihfval  34446  lcfl7N  34716  lcfrlem8  34764  lcfrlem9  34765  lcf1o  34766  hvmapval  34975  hdmap1fval  35012  hdmapffval  35044  hdmapfval  35045  hgmapffval  35103  hgmapfval  35104