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

Theorem mpteq2ia 4251
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 2404 . . 3  |-  A  =  A
21ax-gen 1552 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2731 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4245 . 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 2666    e. cmpt 4226
This theorem is referenced by:  mpteq2i  4252  feqresmpt  5739  fmptap  5882  offres  6278  resixpfo  7059  dfoi  7436  cantnflem1d  7600  cantnflem1  7601  cnrecnv  11925  ackbijnn  12562  harmonic  12593  ege2le3  12647  eirrlem  12758  prmrec  13245  imasdsval2  13697  cayleylem1  15065  gsumzsplit  15484  gsumsn  15498  gsum2d  15501  dmdprdsplitlem  15550  coe1sclmul  16629  coe1sclmul2  16631  leordtvallem1  17228  leordtvallem2  17229  txkgen  17637  cnmpt1st  17653  cnmpt2nd  17654  tmdgsum  18078  tsmssplit  18134  cnfldnm  18766  expcn  18855  pcorev2  19006  pi1xfrcnv  19035  mbfi1flim  19568  itg2uba  19588  itg2cnlem1  19606  itg2cnlem2  19607  itgitg2  19651  itgss3  19659  itgless  19661  ibladdlem  19664  itgaddlem1  19667  iblabslem  19672  itggt0  19686  itgcn  19687  limcdif  19716  limcres  19726  cnplimc  19727  dvcobr  19785  dvexp  19792  dveflem  19816  dvef  19817  dvlip  19830  dvlipcn  19831  lhop  19853  tdeglem2  19937  plyid  20081  coeidp  20134  dgrid  20135  pserdvlem2  20297  abelth  20310  dvrelog  20481  logcn  20491  dvlog  20495  advlog  20498  advlogexp  20499  logtayl  20504  logccv  20507  dvcxp1  20579  dvsqr  20581  resqrcn  20586  loglesqr  20595  dvatan  20728  leibpilem2  20734  leibpi  20735  efrlim  20761  sqrlim  20764  amgmlem  20781  emcllem5  20791  chtublem  20948  logfacrlim2  20963  bposlem6  21026  chto1lb  21125  vmadivsum  21129  dchrvmasumlema  21147  mulogsumlem  21178  logdivsum  21180  logsqvma2  21190  log2sumbnd  21191  selberglem1  21192  selberglem3  21194  selberg  21195  selberg2lem  21197  selberg2  21198  pntrmax  21211  pntrsumo1  21212  selbergr  21215  selbergs  21221  pnt2  21260  pnt  21261  ostth2  21284  ostth  21286  hilnormi  22618  bra0  23406  partfun  24040  zrhre  24338  qqhre  24339  lgamgulmlem2  24767  lgam1  24801  faclim  25313  ovoliunnfl  26147  voliunnfl  26149  mbfposadd  26153  itg2addnclem  26155  ibladdnclem  26160  itgaddnclem1  26162  iblabsnclem  26167  itggt0cn  26176  dvreasin  26179  dvreacos  26180  areacirclem2  26181  lhe4.4ex1a  27414  itgsin0pilem1  27611  wallispilem4  27684  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-ral 2671  df-opab 4227  df-mpt 4228
  Copyright terms: Public domain W3C validator