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

Theorem mpteq2ia 4103
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 2284 . . 3  |-  A  =  A
21ax-gen 1534 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2609 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4097 . 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 6   A.wal 1528    = wceq 1624    e. wcel 1685   A.wral 2544    e. cmpt 4078
This theorem is referenced by:  mpteq2i  4104  feqresmpt  5537  fmptap  5671  offres  6053  resixpfo  6849  dfoi  7221  cantnflem1d  7385  cantnflem1  7386  cnrecnv  11644  ackbijnn  12280  harmonic  12311  ege2le3  12365  eirrlem  12476  prmrec  12963  imasdsval2  13413  cayleylem1  14781  gsumzsplit  15200  gsumsn  15214  gsum2d  15217  dmdprdsplitlem  15266  coe1sclmul  16352  coe1sclmul2  16354  leordtvallem1  16934  leordtvallem2  16935  txkgen  17340  cnmpt1st  17356  cnmpt2nd  17357  tmdgsum  17772  tsmssplit  17828  cnfldnm  18282  expcn  18370  pcorev2  18520  pi1xfrcnv  18549  mbfi1flim  19072  itg2uba  19092  itg2cnlem1  19110  itg2cnlem2  19111  itgitg2  19155  itgss3  19163  itgless  19165  ibladdlem  19168  itgaddlem1  19171  iblabslem  19176  itggt0  19190  itgcn  19191  limcdif  19220  limcres  19230  cnplimc  19231  dvcobr  19289  dvexp  19296  dveflem  19320  dvef  19321  dvlip  19334  dvlipcn  19335  lhop  19357  tdeglem2  19441  plyid  19585  coeidp  19638  dgrid  19639  pserdvlem2  19798  abelth  19811  dvrelog  19978  logcn  19988  dvlog  19992  advlog  19995  advlogexp  19996  logtayl  20001  logccv  20004  dvcxp1  20076  dvsqr  20078  resqrcn  20083  loglesqr  20092  dvatan  20225  leibpilem2  20231  leibpi  20232  efrlim  20258  sqrlim  20261  amgmlem  20278  emcllem5  20287  chtublem  20444  logfacrlim2  20459  bposlem6  20522  chto1lb  20621  vmadivsum  20625  dchrvmasumlema  20643  mulogsumlem  20674  logdivsum  20676  logsqvma2  20686  log2sumbnd  20687  selberglem1  20688  selberglem3  20690  selberg  20691  selberg2lem  20693  selberg2  20694  pntrmax  20707  pntrsumo1  20708  selbergr  20711  selbergs  20717  pnt2  20756  pnt  20757  ostth2  20780  ostth  20782  hilnormi  21734  bra0  22522  svs2  24886  svs3  24887  lhe4.4ex1a  26945  itgsin0pilem1  27143  wallispilem4  27216  wallispi2  27221  stirlinglem1  27222  stirlinglem3  27224
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-ral 2549  df-opab 4079  df-mpt 4080
  Copyright terms: Public domain W3C validator