MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq2ia Unicode version

Theorem mpteq2ia 4233
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Hypothesis
Ref Expression
mpteq2ia.1  |-  ( x  e.  A  ->  B  =  C )
Assertion
Ref Expression
mpteq2ia  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )

Proof of Theorem mpteq2ia
StepHypRef Expression
1 eqid 2388 . . 3  |-  A  =  A
21ax-gen 1552 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2715 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4227 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 654 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546    = wceq 1649    e. wcel 1717   A.wral 2650    e. cmpt 4208
This theorem is referenced by:  mpteq2i  4234  feqresmpt  5720  fmptap  5863  offres  6259  resixpfo  7037  dfoi  7414  cantnflem1d  7578  cantnflem1  7579  cnrecnv  11898  ackbijnn  12535  harmonic  12566  ege2le3  12620  eirrlem  12731  prmrec  13218  imasdsval2  13670  cayleylem1  15038  gsumzsplit  15457  gsumsn  15471  gsum2d  15474  dmdprdsplitlem  15523  coe1sclmul  16602  coe1sclmul2  16604  leordtvallem1  17197  leordtvallem2  17198  txkgen  17606  cnmpt1st  17622  cnmpt2nd  17623  tmdgsum  18047  tsmssplit  18103  cnfldnm  18685  expcn  18774  pcorev2  18925  pi1xfrcnv  18954  mbfi1flim  19483  itg2uba  19503  itg2cnlem1  19521  itg2cnlem2  19522  itgitg2  19566  itgss3  19574  itgless  19576  ibladdlem  19579  itgaddlem1  19582  iblabslem  19587  itggt0  19601  itgcn  19602  limcdif  19631  limcres  19641  cnplimc  19642  dvcobr  19700  dvexp  19707  dveflem  19731  dvef  19732  dvlip  19745  dvlipcn  19746  lhop  19768  tdeglem2  19852  plyid  19996  coeidp  20049  dgrid  20050  pserdvlem2  20212  abelth  20225  dvrelog  20396  logcn  20406  dvlog  20410  advlog  20413  advlogexp  20414  logtayl  20419  logccv  20422  dvcxp1  20494  dvsqr  20496  resqrcn  20501  loglesqr  20510  dvatan  20643  leibpilem2  20649  leibpi  20650  efrlim  20676  sqrlim  20679  amgmlem  20696  emcllem5  20706  chtublem  20863  logfacrlim2  20878  bposlem6  20941  chto1lb  21040  vmadivsum  21044  dchrvmasumlema  21062  mulogsumlem  21093  logdivsum  21095  logsqvma2  21105  log2sumbnd  21106  selberglem1  21107  selberglem3  21109  selberg  21110  selberg2lem  21112  selberg2  21113  pntrmax  21126  pntrsumo1  21127  selbergr  21130  selbergs  21136  pnt2  21175  pnt  21176  ostth2  21199  ostth  21201  hilnormi  22514  bra0  23302  partfun  23929  zrhre  24182  qqhre  24183  lgamgulmlem2  24594  lgam1  24628  faclim  25124  ovoliunnfl  25954  voliunnfl  25956  itg2addnclem  25958  ibladdnclem  25962  itgaddnclem1  25964  iblabsnclem  25969  itggt0cn  25978  dvreasin  25981  dvreacos  25982  areacirclem2  25983  lhe4.4ex1a  27216  itgsin0pilem1  27413  wallispilem4  27486  wallispi2  27491  stirlinglem1  27492  stirlinglem3  27494
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
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 2375  df-cleq 2381  df-clel 2384  df-ral 2655  df-opab 4209  df-mpt 4210
  Copyright terms: Public domain W3C validator