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

Theorem mpteq2ia 4204
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 2366 . . 3  |-  A  =  A
21ax-gen 1551 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2693 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4198 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 653 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1545    = wceq 1647    e. wcel 1715   A.wral 2628    e. cmpt 4179
This theorem is referenced by:  mpteq2i  4205  feqresmpt  5683  fmptap  5823  offres  6219  resixpfo  6997  dfoi  7373  cantnflem1d  7537  cantnflem1  7538  cnrecnv  11857  ackbijnn  12494  harmonic  12525  ege2le3  12579  eirrlem  12690  prmrec  13177  imasdsval2  13629  cayleylem1  14997  gsumzsplit  15416  gsumsn  15430  gsum2d  15433  dmdprdsplitlem  15482  coe1sclmul  16568  coe1sclmul2  16570  leordtvallem1  17157  leordtvallem2  17158  txkgen  17563  cnmpt1st  17579  cnmpt2nd  17580  tmdgsum  17991  tsmssplit  18047  cnfldnm  18501  expcn  18590  pcorev2  18741  pi1xfrcnv  18770  mbfi1flim  19293  itg2uba  19313  itg2cnlem1  19331  itg2cnlem2  19332  itgitg2  19376  itgss3  19384  itgless  19386  ibladdlem  19389  itgaddlem1  19392  iblabslem  19397  itggt0  19411  itgcn  19412  limcdif  19441  limcres  19451  cnplimc  19452  dvcobr  19510  dvexp  19517  dveflem  19541  dvef  19542  dvlip  19555  dvlipcn  19556  lhop  19578  tdeglem2  19662  plyid  19806  coeidp  19859  dgrid  19860  pserdvlem2  20022  abelth  20035  dvrelog  20206  logcn  20216  dvlog  20220  advlog  20223  advlogexp  20224  logtayl  20229  logccv  20232  dvcxp1  20304  dvsqr  20306  resqrcn  20311  loglesqr  20320  dvatan  20453  leibpilem2  20459  leibpi  20460  efrlim  20486  sqrlim  20489  amgmlem  20506  emcllem5  20516  chtublem  20673  logfacrlim2  20688  bposlem6  20751  chto1lb  20850  vmadivsum  20854  dchrvmasumlema  20872  mulogsumlem  20903  logdivsum  20905  logsqvma2  20915  log2sumbnd  20916  selberglem1  20917  selberglem3  20919  selberg  20920  selberg2lem  20922  selberg2  20923  pntrmax  20936  pntrsumo1  20937  selbergr  20940  selbergs  20946  pnt2  20985  pnt  20986  ostth2  21009  ostth  21011  hilnormi  22176  bra0  22964  partfun  23611  zrhre  23972  qqhre  23973  lgamgulmlem2  24383  lgam1  24417  faclim  24925  ovoliunnfl  25756  voliunnfl  25758  itg2addnclem  25760  ibladdnclem  25764  itgaddnclem1  25766  iblabsnclem  25771  itggt0cn  25780  dvreasin  25783  dvreacos  25784  areacirclem2  25785  lhe4.4ex1a  27137  itgsin0pilem1  27335  wallispilem4  27408  wallispi2  27413  stirlinglem1  27414  stirlinglem3  27416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-ral 2633  df-opab 4180  df-mpt 4181
  Copyright terms: Public domain W3C validator