Theorem mpteq2dv 4400

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

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   e. cmpt 4371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-ral 2741  df-opab 4372  df-mpt 4373

This theorem is referenced by:  ofeq  6343  mpt2curryvald  6810  rdgeq1  6888  rdgeq2  6889  omv  6973  oev  6975  oieq1  7747  oieq2  7748  cantnffvalOLD  7892  cantnflem1  7918  cantnflem1OLD  7941  wunex2  8926  wuncval2  8935  reexALT  11006  seqof2  11885  limsupval  12973  sumeq2w  13190  sumeq2ii  13191  cbvsum  13193  summo  13215  fsum  13218  fsumrlim  13295  fsumo1  13296  rpnnen2lem1  13518  rpnnen2lem2  13519  rpnnen  13530  1arithlem1  14005  vdwapval  14055  vdwlem6  14068  vdwlem8  14070  vdwlem9  14071  vdwlem10  14072  ramub1lem2  14109  ramcl  14111  prdsplusgval  14432  prdsmulrval  14434  prdsdsval  14437  prdsvscaval  14438  ismon  14693  fucco  14893  curf1  15056  curf2  15060  yonedalem4a  15106  grplactfval  15643  galactghm  15929  pmtrval  15978  sylow1  16123  sylow2b  16143  sylow3lem5  16151  sylow3  16153  iscyg  16377  gsumzaddlem  16429  gsumzaddlemOLD  16431  gsumzmhm  16452  gsumzmhmOLD  16453  ablfac2  16612  gsumdixpOLD  16722  gsumdixp  16723  fczpsrbag  17456  psrmulfval  17478  mvrval  17516  subrgmvr  17562  mplcoe1  17566  mplcoe3  17567  mplcoe3OLD  17568  mplcoe5  17570  mplcoe2OLD  17572  mplmon2  17597  subrgascl  17602  evlslem2  17619  evlslem3  17622  evlslem1  17623  mpfrcl  17626  evlsval  17627  evlsvar  17631  mpfind  17644  coe1fval  17683  pf1ind  17811  evl1gsumadd  17814  zncyg  18003  phllmhm  18083  isphld  18105  frlmgsumOLD  18217  frlmgsum  18218  frlmipval  18226  frlmphl  18228  uvcval  18232  mamuval  18306  mamufv  18307  madetsumid  18368  mvmulval  18376  mvmulfv  18377  mavmulfv  18379  1mavmul  18381  marepvval0  18399  mulmarep1gsum1  18406  mdetleib  18420  mdetleib2  18421  mdetfval1  18423  mdetleib1  18424  mdet0pr  18425  mdetralt  18436  mdetunilem9  18448  m2detleib  18459  smadiadetlem3  18496  ptbasfi  19176  ptcnplem  19216  ptrescn  19234  cnmpt2k  19283  xkohmeo  19410  fmval  19538  fmf  19540  ptcmpg  19651  tmdmulg  19685  prdstmdd  19716  tsmspropd  19724  prdsxmslem2  20126  metdsval  20445  fsumcn  20468  expcn  20470  lebnumlem3  20557  pcoval  20605  pi1xfrcnv  20651  rrxds  20919  rrxmval  20926  itg11  21191  mbfi1fseqlem2  21216  mbfi1fseqlem6  21220  mbfi1fseq  21221  mbfi1flimlem  21222  mbfmullem  21225  itg2const  21240  itg2mulc  21247  itg2monolem1  21250  itg2i1fseqle  21254  itg2i1fseq  21255  itg2addlem  21258  itg2cnlem1  21261  itg2cn  21263  isibl  21265  isibl2  21266  iblitg  21268  itgz  21280  itgvallem  21284  itgvallem3  21285  iblcnlem1  21287  itgcnlem  21289  iblrelem  21290  iblposlem  21291  iblpos  21292  itgrevallem1  21294  itgposval  21295  iblss2  21305  itgss  21311  itgfsum  21326  iblabslem  21327  iblmulc2  21330  bddmulibl  21338  itgcn  21342  ellimc  21370  dvnfval  21418  cpnfval  21428  dvexp  21449  dvexp2  21450  dvmptfsum  21469  dvlipcn  21488  dvivthlem1  21502  dvfsumle  21515  dvfsumabs  21517  dvfsumlem2  21521  elply2  21686  elplyr  21691  elplyd  21692  coeeu  21715  coelem  21716  coeeq  21717  plyco  21731  coe11  21742  coe1termlem  21747  dgrcolem1  21762  dvply2g  21773  elqaalem3  21809  eltayl  21847  tayl0  21849  taylthlem1  21860  taylthlem2  21861  ulmcau  21882  ulmdvlem1  21887  ulmdvlem3  21889  mtest  21891  mtestbdd  21892  pserval  21897  pserulm  21909  psercn  21913  pserdvlem2  21915  abelthlem3  21920  logtayl  22127  dvcxp1  22202  dmarea  22373  musum  22553  dchrptlem2  22626  dchrptlem3  22627  dchrpt  22628  lgsval  22661  lgsval4lem  22668  lgsneg  22680  lgsmod  22682  rpvmasum2  22783  padicfval  22887  ostth2  22908  ostth3  22909  ostth  22910  htthlem  24341  htth  24342  pjhfval  24821  hosmval  25161  hommval  25162  hodmval  25163  hfsmval  25164  hfmmval  25165  brafval  25369  kbfval  25378  indval  26492  ofceq  26561  itgeq12dv  26734  ballotlemfval  26894  lgamgulmlem2  27038  lgamgulmlem5  27041  ptpcon  27144  cvmliftlem15  27209  cvmlift2lem4  27217  cvmlift2  27227  snmlval  27242  snmlflim  27243  relexp0  27353  relexpsucr  27354  prodeq2w  27447  prodmo  27471  fprod  27476  faclim  27574  faclim2  27576  trpredeq1  27706  trpredeq2  27707  bpolylem  28213  voliunnfl  28461  itg2addnclem  28469  itg2addnclem3  28471  itg2addnc  28472  itg2gt0cn  28473  iblabsnclem  28481  iblmulc2nc  28483  ftc1anclem2  28494  ftc1anclem6  28498  ftc1anclem8  28500  ftc1anc  28501  ftc2nc  28502  dvcncxp1  28503  upixp  28649  rrncmslem  28757  ismrer1  28763  mzpclval  29087  mzpcl2  29092  mzpexpmpt  29107  mzpsubst  29111  mzpcompact2lem  29114  rmxfval  29271  rmyfval  29272  aomclem8  29440  hbtlem1  29505  hbtlem7  29507  itgpowd  29616  expgrowthi  29633  expgrowth  29635  addrval  29748  subrval  29749  mulvval  29750  fmulcl  29788  fmuldfeqlem1  29789  stoweidlem2  29823  stoweidlem17  29838  stoweidlem19  29840  stoweidlem20  29841  stoweidlem43  29864  stoweidlem62  29883  stoweid  29884  wwlkn  30342  clwwlkn  30456  clwwlknprop  30461  matgsum  30900  mat1dimmul  30911  m1detdiag  30931  lincop  30939  mat2pmatmhmlem1  31082  mply1topmatval  31109  pmatcollpw1dst  31116  pmatcollpw1  31119  pmattomply1  31126  mp2pm2mplem1  31131  mp2pm2mplem3  31133  pmattomply1fo  31138  tendoplcbv  34515  tendopl  34516  tendoicbv  34533  tendoi  34534  dihfval  34972  lcfl7N  35242  lcfrlem8  35290  lcfrlem9  35291  lcf1o  35292  hvmapval  35501  hdmap1fval  35538  hdmapffval  35570  hdmapfval  35571  hgmapffval  35629  hgmapfval  35630