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

Theorem mpteq2ia 4259
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 2412 . . 3  |-  A  =  A
21ax-gen 1552 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2739 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4253 . 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 1546    = wceq 1649    e. wcel 1721   A.wral 2674    e. cmpt 4234
This theorem is referenced by:  mpteq2i  4260  feqresmpt  5747  fmptap  5890  offres  6286  resixpfo  7067  dfoi  7444  cantnflem1d  7608  cantnflem1  7609  cnrecnv  11933  ackbijnn  12570  harmonic  12601  ege2le3  12655  eirrlem  12766  prmrec  13253  imasdsval2  13705  cayleylem1  15073  gsumzsplit  15492  gsumsn  15506  gsum2d  15509  dmdprdsplitlem  15558  coe1sclmul  16637  coe1sclmul2  16639  leordtvallem1  17236  leordtvallem2  17237  txkgen  17645  cnmpt1st  17661  cnmpt2nd  17662  tmdgsum  18086  tsmssplit  18142  cnfldnm  18774  expcn  18863  pcorev2  19014  pi1xfrcnv  19043  mbfi1flim  19576  itg2uba  19596  itg2cnlem1  19614  itg2cnlem2  19615  itgitg2  19659  itgss3  19667  itgless  19669  ibladdlem  19672  itgaddlem1  19675  iblabslem  19680  itggt0  19694  itgcn  19695  limcdif  19724  limcres  19734  cnplimc  19735  dvcobr  19793  dvexp  19800  dveflem  19824  dvef  19825  dvlip  19838  dvlipcn  19839  lhop  19861  tdeglem2  19945  plyid  20089  coeidp  20142  dgrid  20143  pserdvlem2  20305  abelth  20318  dvrelog  20489  logcn  20499  dvlog  20503  advlog  20506  advlogexp  20507  logtayl  20512  logccv  20515  dvcxp1  20587  dvsqr  20589  resqrcn  20594  loglesqr  20603  dvatan  20736  leibpilem2  20742  leibpi  20743  efrlim  20769  sqrlim  20772  amgmlem  20789  emcllem5  20799  chtublem  20956  logfacrlim2  20971  bposlem6  21034  chto1lb  21133  vmadivsum  21137  dchrvmasumlema  21155  mulogsumlem  21186  logdivsum  21188  logsqvma2  21198  log2sumbnd  21199  selberglem1  21200  selberglem3  21202  selberg  21203  selberg2lem  21205  selberg2  21206  pntrmax  21219  pntrsumo1  21220  selbergr  21223  selbergs  21229  pnt2  21268  pnt  21269  ostth2  21292  ostth  21294  hilnormi  22626  bra0  23414  partfun  24048  zrhre  24346  qqhre  24347  lgamgulmlem2  24775  lgam1  24809  faclim  25321  ovoliunnfl  26155  voliunnfl  26157  mbfposadd  26161  itg2addnclem  26163  ibladdnclem  26168  itgaddnclem1  26170  iblabsnclem  26175  itggt0cn  26184  dvreasin  26187  dvreacos  26188  areacirclem2  26189  lhe4.4ex1a  27422  itgsin0pilem1  27619  wallispilem4  27692  wallispi2  27697  stirlinglem1  27698  stirlinglem3  27700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-ral 2679  df-opab 4235  df-mpt 4236
  Copyright terms: Public domain W3C validator