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

Theorem mpteq2ia 4102
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 2283 . . 3  |-  A  =  A
21ax-gen 1533 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2608 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4096 . 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 1527    = wceq 1623    e. wcel 1684   A.wral 2543    e. cmpt 4077
This theorem is referenced by:  mpteq2i  4103  feqresmpt  5576  fmptap  5710  offres  6092  resixpfo  6854  dfoi  7226  cantnflem1d  7390  cantnflem1  7391  cnrecnv  11650  ackbijnn  12286  harmonic  12317  ege2le3  12371  eirrlem  12482  prmrec  12969  imasdsval2  13419  cayleylem1  14787  gsumzsplit  15206  gsumsn  15220  gsum2d  15223  dmdprdsplitlem  15272  coe1sclmul  16358  coe1sclmul2  16360  leordtvallem1  16940  leordtvallem2  16941  txkgen  17346  cnmpt1st  17362  cnmpt2nd  17363  tmdgsum  17778  tsmssplit  17834  cnfldnm  18288  expcn  18376  pcorev2  18526  pi1xfrcnv  18555  mbfi1flim  19078  itg2uba  19098  itg2cnlem1  19116  itg2cnlem2  19117  itgitg2  19161  itgss3  19169  itgless  19171  ibladdlem  19174  itgaddlem1  19177  iblabslem  19182  itggt0  19196  itgcn  19197  limcdif  19226  limcres  19236  cnplimc  19237  dvcobr  19295  dvexp  19302  dveflem  19326  dvef  19327  dvlip  19340  dvlipcn  19341  lhop  19363  tdeglem2  19447  plyid  19591  coeidp  19644  dgrid  19645  pserdvlem2  19804  abelth  19817  dvrelog  19984  logcn  19994  dvlog  19998  advlog  20001  advlogexp  20002  logtayl  20007  logccv  20010  dvcxp1  20082  dvsqr  20084  resqrcn  20089  loglesqr  20098  dvatan  20231  leibpilem2  20237  leibpi  20238  efrlim  20264  sqrlim  20267  amgmlem  20284  emcllem5  20293  chtublem  20450  logfacrlim2  20465  bposlem6  20528  chto1lb  20627  vmadivsum  20631  dchrvmasumlema  20649  mulogsumlem  20680  logdivsum  20682  logsqvma2  20692  log2sumbnd  20693  selberglem1  20694  selberglem3  20696  selberg  20697  selberg2lem  20699  selberg2  20700  pntrmax  20713  pntrsumo1  20714  selbergr  20717  selbergs  20723  pnt2  20762  pnt  20763  ostth2  20786  ostth  20788  hilnormi  21742  bra0  22530  dvreasin  24334  dvreacos  24335  areacirclem2  24337  svs2  24899  svs3  24900  lhe4.4ex1a  26958  itgsin0pilem1  27156  wallispilem4  27229  wallispi2  27234  stirlinglem1  27235  stirlinglem3  27237
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator