Theorem mpteq2dv 4511

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

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1872   |-> cmpt 4482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-ral 2776  df-opab 4483  df-mpt 4484

This theorem is referenced by:  ofeq  6547  mpt2curryvald  7028  rdgeq1  7140  rdgeq2  7141  omv  7225  oev  7227  oieq1  8036  oieq2  8037  cantnflem1  8202  wunex2  9170  wuncval2  9179  reexALT  11303  seqof2  12277  relexpsucnnr  13088  relexp1g  13089  limsupval  13530  limsupvalOLD  13531  sumeq2w  13757  sumeq2ii  13758  cbvsum  13760  summo  13782  fsum  13785  fsumrlim  13870  fsumo1  13871  prodeq2w  13965  prodmo  13989  fprod  13994  bpolylem  14100  rpnnen2lem1  14266  rpnnen2lem2  14267  rpnnen  14278  1arithlem1  14866  vdwapval  14922  vdwlem6  14935  vdwlem8  14937  vdwlem9  14938  vdwlem10  14939  ramub1lem2  14984  ramcl  14986  prdsplusgval  15370  prdsmulrval  15372  prdsdsval  15375  prdsvscaval  15376  ismon  15637  fucco  15866  curf1  16109  curf2  16113  yonedalem4a  16159  grplactfval  16751  galactghm  17043  pmtrval  17091  sylow1  17254  sylow2b  17274  sylow3lem5  17282  sylow3  17284  iscyg  17513  gsumzaddlem  17553  gsumzmhm  17569  ablfac2  17721  gsumdixp  17836  fczpsrbag  18590  psrmulfval  18608  mvrval  18644  subrgmvr  18684  mplcoe1  18688  mplcoe3  18689  mplcoe5  18691  mplmon2  18715  subrgascl  18720  evlslem2  18734  evlslem3  18736  evlslem1  18737  mpfrcl  18740  evlsval  18741  evlsvar  18745  mpfind  18758  coe1fval  18797  pf1ind  18942  evl1gsumadd  18945  zncyg  19117  phllmhm  19197  isphld  19219  frlmgsum  19328  frlmipval  19335  frlmphl  19337  uvcval  19341  mamuval  19409  mamufv  19410  matgsum  19460  madetsumid  19484  mat1dimmul  19499  mvmulval  19566  mvmulfv  19567  mavmulfv  19569  1mavmul  19571  marepvval0  19589  mulmarep1gsum1  19596  mdetleib  19610  mdetleib2  19611  mdetfval1  19613  mdetleib1  19614  mdet0pr  19615  m1detdiag  19620  mdetralt  19631  mdetunilem9  19643  m2detleib  19654  smadiadetlem3  19691  mat2pmatmul  19753  decpmatmul  19794  decpmatmulsumfsupp  19795  pmatcollpw1  19798  monmatcollpw  19801  pmatcollpw3lem  19805  pmatcollpw3fi1lem2  19809  pm2mpval  19817  pm2mpfval  19818  mply1topmatval  19826  mp2pm2mplem1  19828  mp2pm2mplem3  19830  ptbasfi  20594  ptcnplem  20634  ptrescn  20652  cnmpt2k  20701  xkohmeo  20828  fmval  20956  fmf  20958  ptcmpg  21070  tmdmulg  21105  prdstmdd  21136  tsmspropd  21144  prdsxmslem2  21542  metdsval  21862  metdsvalOLD  21877  fsumcn  21900  expcn  21902  lebnumlem3  21989  lebnumlem3OLD  21992  pcoval  22040  pi1xfrcnv  22086  rrxds  22350  rrxmval  22357  itg11  22647  mbfi1fseqlem2  22672  mbfi1fseqlem6  22676  mbfi1fseq  22677  mbfi1flimlem  22678  mbfmullem  22681  itg2const  22696  itg2mulc  22703  itg2monolem1  22706  itg2i1fseqle  22710  itg2i1fseq  22711  itg2addlem  22714  itg2cnlem1  22717  itg2cn  22719  isibl  22721  isibl2  22722  iblitg  22724  itgz  22736  itgvallem  22740  itgvallem3  22741  iblcnlem1  22743  itgcnlem  22745  iblrelem  22746  iblposlem  22747  iblpos  22748  itgrevallem1  22750  itgposval  22751  iblss2  22761  itgss  22767  itgfsum  22782  iblabslem  22783  iblmulc2  22786  bddmulibl  22794  itgcn  22798  ellimc  22826  dvnfval  22874  cpnfval  22884  dvexp  22905  dvexp2  22906  dvmptfsum  22925  dvlipcn  22944  dvivthlem1  22958  dvfsumle  22971  dvfsumabs  22973  dvfsumlem2  22977  elply2  23148  elplyr  23153  elplyd  23154  coeeu  23177  coelem  23178  coeeq  23179  plyco  23193  coe11  23205  coe1termlem  23210  dgrcolem1  23225  dvply2g  23236  elqaalem3  23272  elqaalem3OLD  23275  eltayl  23313  tayl0  23315  taylthlem1  23326  taylthlem2  23327  ulmcau  23348  ulmdvlem1  23353  ulmdvlem3  23355  mtest  23357  mtestbdd  23358  pserval  23363  pserulm  23375  psercn  23379  pserdvlem2  23381  abelthlem3  23386  logtayl  23603  dvcxp1  23678  dvcncxp1  23681  logbmpt  23723  dmarea  23881  lgamgulmlem2  23953  lgamgulmlem5  23956  musum  24118  dchrptlem2  24191  dchrptlem3  24192  dchrpt  24193  lgsval  24226  lgsval4lem  24233  lgsneg  24245  lgsmod  24247  rpvmasum2  24348  padicfval  24452  ostth2  24473  ostth3  24474  ostth  24475  lmif  24825  islmib  24827  wwlkn  25408  clwwlkn  25493  clwwlknprop  25498  htthlem  26568  htth  26569  pjhfval  27047  hosmval  27386  hommval  27387  hodmval  27388  hfsmval  27389  hfmmval  27390  brafval  27594  kbfval  27603  psgnfzto1st  28626  mdetpmtr1  28657  ordtcnvNEW  28734  ordtrest2NEW  28737  xrhval  28830  indval  28843  esum2dlem  28921  ofceq  28926  itgeq12dv  29167  ballotlemfval  29330  ptpcon  29964  cvmliftlem15  30029  cvmlift2lem4  30037  cvmlift2  30047  snmlval  30062  snmlflim  30063  mrsubfval  30154  mrsubrn  30159  elmsubrn  30174  msubrn  30175  msubco  30177  faclim  30389  faclim2  30391  trpredeq1  30468  trpredeq2  30469  csbrdgg  31694  poimirlem5  31909  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem10  31914  poimirlem11  31915  poimirlem12  31916  poimirlem15  31919  poimirlem16  31920  poimirlem17  31921  poimirlem18  31922  poimirlem19  31923  poimirlem20  31924  poimirlem21  31925  poimirlem22  31926  poimirlem27  31931  voliunnfl  31948  itg2addnclem  31957  itg2addnclem3  31959  itg2addnc  31960  itg2gt0cn  31961  iblabsnclem  31969  iblmulc2nc  31971  ftc1anclem2  31982  ftc1anclem6  31986  ftc1anclem8  31988  ftc1anc  31989  ftc2nc  31990  upixp  32020  rrncmslem  32128  ismrer1  32134  tendoplcbv  34311  tendopl  34312  tendoicbv  34329  tendoi  34330  dihfval  34768  lcfl7N  35038  lcfrlem8  35086  lcfrlem9  35087  lcf1o  35088  hvmapval  35297  hdmap1fval  35334  hdmapffval  35366  hdmapfval  35367  hgmapffval  35425  hgmapfval  35426  mzpclval  35536  mzpcl2  35541  mzpexpmpt  35556  mzpsubst  35559  mzpcompact2lem  35562  rmxfval  35722  rmyfval  35723  aomclem8  35889  hbtlem1  35952  hbtlem7  35954  itgpowd  36069  expgrowthi  36652  expgrowth  36654  binomcxplemdvsum  36674  addrval  36789  subrval  36790  mulvval  36791  fmulcl  37599  fmuldfeqlem1  37600  fprodcncf  37719  dvnmptdivc  37753  dvnxpaek  37757  dvnmul  37758  dvmptfprod  37760  dvnprodlem1  37761  dvnprodlem2  37762  dvnprodlem3  37763  dvnprod  37764  stoweidlem2  37802  stoweidlem17  37817  stoweidlem19  37819  stoweidlem20  37820  stoweidlem43  37844  stoweidlem62  37863  stoweidlem62OLD  37864  stoweid  37865  dirkercncflem2  37906  fourierdlem112  38022  fourierdlem113  38023  etransclem1  38040  etransclem5  38044  etransclem17  38056  etransclem19  38058  etransclem22  38061  sge0val  38116  ovnlecvr  38284  ovncvrrp  38290  ovn0lem  38291  ovnsubaddlem1  38296  ovnsubadd  38298  hsphoif  38302  hsphoival  38305  hoidmv1lelem1  38317  hoidmv1lelem2  38318  hoidmv1lelem3  38319  hoidmv1le  38320  hoidmvlelem1  38321  hoidmvlelem2  38322  hoidmvlelem3  38323  hoidmvlelem4  38324  hoidmvlelem5  38325  hoidmvle  38326  ovnhoilem1  38327  ovnhoi  38329  incistruhgr  39001  c0rhm  39532  c0rnghm  39533  lincop  39823  aacllem  40162