Theorem mpteq2dv 4256

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 452	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	2	mpteq2dva 4255	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721   e. cmpt 4226

This theorem is referenced by:  ofeq  6266  rdgeq1  6628  rdgeq2  6629  omv  6715  oev  6717  oieq1  7437  oieq2  7438  cantnflem1  7601  wunex2  8569  wuncval2  8578  reexALT  10562  seqof2  11336  limsupval  12223  sumeq2w  12441  cbvsum  12444  summo  12466  fsum  12469  fsumrlim  12545  fsumo1  12546  rpnnen2lem1  12769  rpnnen2lem2  12770  rpnnen  12781  1arithlem1  13246  vdwapval  13296  vdwlem6  13309  vdwlem8  13311  vdwlem9  13312  vdwlem10  13313  ramub1lem2  13350  ramcl  13352  prdsplusgval  13650  prdsmulrval  13652  prdsdsval  13655  prdsvscaval  13656  ismon  13914  fucco  14114  curf1  14277  curf2  14281  yonedalem4a  14327  grplactfval  14840  galactghm  15061  sylow1  15192  sylow2b  15212  sylow3lem5  15220  sylow3  15222  iscyg  15444  gsumzaddlem  15481  gsumzmhm  15488  ablfac2  15602  gsumdixp  15670  psrmulfval  16404  mvrval  16440  subrgmvr  16479  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  mplmon2  16508  subrgascl  16513  evlslem2  16523  coe1fval  16558  zncyg  16784  phllmhm  16818  isphld  16840  ptbasfi  17566  ptcnplem  17606  ptrescn  17624  cnmpt2k  17673  xkohmeo  17800  fmval  17928  fmf  17930  ptcmpg  18041  tmdmulg  18075  prdstmdd  18106  tsmspropd  18114  prdsxmslem2  18512  metdsval  18830  fsumcn  18853  expcn  18855  lebnumlem3  18941  pcoval  18989  pi1xfrcnv  19035  itg11  19536  mbfi1fseqlem2  19561  mbfi1fseqlem6  19565  mbfi1fseq  19566  mbfi1flimlem  19567  mbfmullem  19570  itg2const  19585  itg2mulc  19592  itg2monolem1  19595  itg2i1fseqle  19599  itg2i1fseq  19600  itg2addlem  19603  itg2cnlem1  19606  itg2cn  19608  isibl  19610  isibl2  19611  iblitg  19613  itgz  19625  itgvallem  19629  itgvallem3  19630  iblcnlem1  19632  itgcnlem  19634  iblrelem  19635  iblposlem  19636  iblpos  19637  itgrevallem1  19639  itgposval  19640  iblss2  19650  itgss  19656  itgfsum  19671  iblabslem  19672  iblmulc2  19675  bddmulibl  19683  itgcn  19687  ellimc  19713  dvnfval  19761  cpnfval  19771  dvexp  19792  dvexp2  19793  dvmptfsum  19812  dvlipcn  19831  dvivthlem1  19845  dvfsumle  19858  dvfsumabs  19860  dvfsumlem2  19864  evlslem3  19888  evlslem1  19889  mpfrcl  19892  evlsval  19893  evlsvar  19897  mpfind  19918  pf1ind  19928  elply2  20068  elplyr  20073  elplyd  20074  coeeu  20097  coelem  20098  coeeq  20099  plyco  20113  coe11  20124  coe1termlem  20129  dgrcolem1  20144  dvply2g  20155  elqaalem3  20191  eltayl  20229  tayl0  20231  taylthlem1  20242  taylthlem2  20243  ulmcau  20264  ulmdvlem1  20269  ulmdvlem3  20271  mtest  20273  mtestbdd  20274  pserval  20279  pserulm  20291  psercn  20295  pserdvlem2  20297  abelthlem3  20302  logtayl  20504  dvcxp1  20579  dmarea  20749  musum  20929  dchrptlem2  21002  dchrptlem3  21003  dchrpt  21004  lgsval  21037  lgsval4lem  21044  lgsneg  21056  lgsmod  21058  rpvmasum2  21159  padicfval  21263  ostth2  21284  ostth3  21285  ostth  21286  htthlem  22373  htth  22374  pjhfval  22851  hosmval  23191  hommval  23192  hodmval  23193  hfsmval  23194  hfmmval  23195  brafval  23399  kbfval  23408  indval  24364  ofceq  24433  itgeq12dv  24594  ballotlemfval  24700  lgamgulmlem2  24767  lgamgulmlem5  24770  ptpcon  24873  cvmliftlem15  24938  cvmlift2lem4  24946  cvmlift2  24956  snmlval  24971  snmlflim  24972  relexp0  25082  relexpsucr  25083  prodeq2w  25191  prodmo  25215  fprod  25220  faclim  25313  faclim2  25315  trpredeq1  25437  trpredeq2  25438  bpolylem  25998  voliunnfl  26149  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  iblabsnclem  26167  iblmulc2nc  26169  upixp  26321  rrncmslem  26431  ismrer1  26437  mzpclval  26672  mzpcl2  26677  mzpexpmpt  26692  mzpsubst  26695  mzpcompact2lem  26698  rmxfval  26857  rmyfval  26858  aomclem8  27027  frlmgsum  27100  uvcval  27102  hbtlem1  27195  hbtlem7  27197  pmtrval  27262  mamuval  27312  mamufv  27313  mdetleib  27356  expgrowthi  27418  expgrowth  27420  addrval  27538  subrval  27539  mulvval  27540  fmulcl  27578  fmuldfeqlem1  27579  stoweidlem2  27618  stoweidlem17  27633  stoweidlem19  27635  stoweidlem20  27636  stoweidlem43  27659  stoweidlem62  27678  stoweid  27679  tendoplcbv  31257  tendopl  31258  tendoicbv  31275  tendoi  31276  dihfval  31714  lcfl7N  31984  lcfrlem8  32032  lcfrlem9  32033  lcf1o  32034  hvmapval  32243  hdmap1fval  32280  hdmapffval  32312  hdmapfval  32313  hgmapffval  32371  hgmapfval  32372

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-ral 2671  df-opab 4227  df-mpt 4228