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

Theorem mpteq2ia 4278
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 2430 . . 3  |-  A  =  A
21ax-gen 1555 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2758 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4272 . 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 1549    = wceq 1652    e. wcel 1725   A.wral 2692    e. cmpt 4253
This theorem is referenced by:  mpteq2i  4279  feqresmpt  5766  fmptap  5909  offres  6305  resixpfo  7086  dfoi  7464  cantnflem1d  7628  cantnflem1  7629  cnrecnv  11953  ackbijnn  12590  harmonic  12621  ege2le3  12675  eirrlem  12786  prmrec  13273  imasdsval2  13725  cayleylem1  15093  gsumzsplit  15512  gsumsn  15526  gsum2d  15529  dmdprdsplitlem  15578  coe1sclmul  16657  coe1sclmul2  16659  leordtvallem1  17257  leordtvallem2  17258  txkgen  17667  cnmpt1st  17683  cnmpt2nd  17684  tmdgsum  18108  tsmssplit  18164  cnfldnm  18796  expcn  18885  pcorev2  19036  pi1xfrcnv  19065  mbfi1flim  19598  itg2uba  19618  itg2cnlem1  19636  itg2cnlem2  19637  itgitg2  19681  itgss3  19689  itgless  19691  ibladdlem  19694  itgaddlem1  19697  iblabslem  19702  itggt0  19716  itgcn  19717  limcdif  19746  limcres  19756  cnplimc  19757  dvcobr  19815  dvexp  19822  dveflem  19846  dvef  19847  dvlip  19860  dvlipcn  19861  lhop  19883  tdeglem2  19967  plyid  20111  coeidp  20164  dgrid  20165  pserdvlem2  20327  abelth  20340  dvrelog  20511  logcn  20521  dvlog  20525  advlog  20528  advlogexp  20529  logtayl  20534  logccv  20537  dvcxp1  20609  dvsqr  20611  resqrcn  20616  loglesqr  20625  dvatan  20758  leibpilem2  20764  leibpi  20765  efrlim  20791  sqrlim  20794  amgmlem  20811  emcllem5  20821  chtublem  20978  logfacrlim2  20993  bposlem6  21056  chto1lb  21155  vmadivsum  21159  dchrvmasumlema  21177  mulogsumlem  21208  logdivsum  21210  logsqvma2  21220  log2sumbnd  21221  selberglem1  21222  selberglem3  21224  selberg  21225  selberg2lem  21227  selberg2  21228  pntrmax  21241  pntrsumo1  21242  selbergr  21245  selbergs  21251  pnt2  21290  pnt  21291  ostth2  21314  ostth  21316  hilnormi  22648  bra0  23436  partfun  24070  zrhre  24368  qqhre  24369  lgamgulmlem2  24797  lgam1  24831  faclim  25349  ovoliunnfl  26189  voliunnfl  26191  mbfposadd  26195  itg2addnclem  26197  ibladdnclem  26202  itgaddnclem1  26204  iblabsnclem  26209  itggt0cn  26218  dvreasin  26221  dvreacos  26222  areacirclem2  26223  lhe4.4ex1a  27456  itgsin0pilem1  27653  wallispilem4  27726  wallispi2  27731  stirlinglem1  27732  stirlinglem3  27734
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-ral 2697  df-opab 4254  df-mpt 4255
  Copyright terms: Public domain W3C validator