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

Theorem mpteq2ia 4316
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 2442 . . 3  |-  A  =  A
21ax-gen 1556 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2777 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4310 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 655 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550    = wceq 1653    e. wcel 1727   A.wral 2711    e. cmpt 4291
This theorem is referenced by:  mpteq2i  4317  feqresmpt  5809  fmptap  5952  offres  6348  resixpfo  7129  dfoi  7509  cantnflem1d  7673  cantnflem1  7674  cnrecnv  12001  ackbijnn  12638  harmonic  12669  ege2le3  12723  eirrlem  12834  prmrec  13321  imasdsval2  13773  cayleylem1  15141  gsumzsplit  15560  gsumsn  15574  gsum2d  15577  dmdprdsplitlem  15626  coe1sclmul  16705  coe1sclmul2  16707  leordtvallem1  17305  leordtvallem2  17306  txkgen  17715  cnmpt1st  17731  cnmpt2nd  17732  tmdgsum  18156  tsmssplit  18212  cnfldnm  18844  expcn  18933  pcorev2  19084  pi1xfrcnv  19113  mbfi1flim  19644  itg2uba  19664  itg2cnlem1  19682  itg2cnlem2  19683  itgitg2  19727  itgss3  19735  itgless  19737  ibladdlem  19740  itgaddlem1  19743  iblabslem  19748  itggt0  19762  itgcn  19763  limcdif  19794  limcres  19804  cnplimc  19805  dvcobr  19863  dvexp  19870  dveflem  19894  dvef  19895  dvlip  19908  dvlipcn  19909  lhop  19931  tdeglem2  20015  plyid  20159  coeidp  20212  dgrid  20213  pserdvlem2  20375  abelth  20388  dvrelog  20559  logcn  20569  dvlog  20573  advlog  20576  advlogexp  20577  logtayl  20582  logccv  20585  dvcxp1  20657  dvsqr  20659  resqrcn  20664  loglesqr  20673  dvatan  20806  leibpilem2  20812  leibpi  20813  efrlim  20839  sqrlim  20842  amgmlem  20859  emcllem5  20869  chtublem  21026  logfacrlim2  21041  bposlem6  21104  chto1lb  21203  vmadivsum  21207  dchrvmasumlema  21225  mulogsumlem  21256  logdivsum  21258  logsqvma2  21268  log2sumbnd  21269  selberglem1  21270  selberglem3  21272  selberg  21273  selberg2lem  21275  selberg2  21276  pntrmax  21289  pntrsumo1  21290  selbergr  21293  selbergs  21299  pnt2  21338  pnt  21339  ostth2  21362  ostth  21364  hilnormi  22696  bra0  23484  partfun  24118  zrhre  24416  qqhre  24417  lgamgulmlem2  24845  lgam1  24879  faclim  25396  ovoliunnfl  26284  voliunnfl  26286  mbfposadd  26290  dvtan  26293  itg2addnclem  26294  ibladdnclem  26299  itgaddnclem1  26301  iblabsnclem  26306  itggt0cn  26315  ftc1anclem4  26321  ftc1anclem5  26322  ftc1anclem6  26323  ftc1anclem7  26324  ftc1anclem8  26325  dvreasin  26328  dvreacos  26329  areacirclem1  26330  lhe4.4ex1a  27561  itgsin0pilem1  27758  wallispilem4  27831  wallispi2  27836  stirlinglem1  27837  stirlinglem3  27839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2716  df-opab 4292  df-mpt 4293
  Copyright terms: Public domain W3C validator