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

Theorem mpteq2ia 4529
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 2467 . . 3  |-  A  =  A
21ax-gen 1601 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2824 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4523 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 672 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377    = wceq 1379    e. wcel 1767   A.wral 2814    |-> cmpt 4505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-opab 4506  df-mpt 4507
This theorem is referenced by:  mpteq2i  4530  feqresmpt  5921  elfvmptrab  5971  fmptap  6084  offres  6779  resixpfo  7507  dfoi  7936  cantnflem1d  8107  cantnflem1  8108  cantnflem1dOLD  8130  cantnflem1OLD  8131  dfceil2  11936  cnrecnv  12961  ackbijnn  13603  harmonic  13633  ege2le3  13687  eirrlem  13798  prmrec  14299  imasdsval2  14771  cayleylem1  16242  pmtrprfval  16318  gsumzsplit  16747  gsumzsplitOLD  16748  gsum2dlem2  16801  gsum2dOLD  16803  dmdprdsplitlem  16886  dmdprdsplitlemOLD  16887  coe1sclmul  18122  coe1sclmul2  18124  frlmip  18604  mdetunilem9  18917  leordtvallem1  19505  leordtvallem2  19506  txkgen  19916  cnmpt1st  19932  cnmpt2nd  19933  tmdgsum  20357  tsmssplit  20417  cnfldnm  21049  expcn  21139  pcorev2  21291  pi1xfrcnv  21320  rrxip  21585  mbfi1flim  21893  itg2uba  21913  itg2cnlem1  21931  itg2cnlem2  21932  itgitg2  21976  itgss3  21984  itgless  21986  ibladdlem  21989  itgaddlem1  21992  iblabslem  21997  itggt0  22011  itgcn  22012  limcdif  22043  limcres  22053  cnplimc  22054  dvcobr  22112  dvexp  22119  dveflem  22143  dvef  22144  dvlip  22157  dvlipcn  22158  lhop  22180  tdeglem2  22222  mdegfvalOLD  22224  plyid  22369  coeidp  22422  dgrid  22423  pserdvlem2  22585  abelth  22598  dvrelog  22774  logcn  22784  dvlog  22788  advlog  22791  advlogexp  22792  logtayl  22797  logccv  22800  dvcxp1  22872  dvsqrt  22874  resqrtcn  22879  loglesqrt  22888  dvatan  23022  leibpilem2  23028  leibpi  23029  efrlim  23055  sqrtlim  23058  amgmlem  23075  emcllem5  23085  chtublem  23242  logfacrlim2  23257  bposlem6  23320  chto1lb  23419  vmadivsum  23423  dchrvmasumlema  23441  mulogsumlem  23472  logdivsum  23474  logsqvma2  23484  log2sumbnd  23485  selberglem1  23486  selberglem3  23488  selberg  23489  selberg2lem  23491  selberg2  23492  pntrmax  23505  pntrsumo1  23506  selbergr  23509  selbergs  23515  pnt2  23554  pnt  23555  ostth2  23578  ostth  23580  hilnormi  25784  bra0  26573  partfun  27216  zrhre  27661  qqhre  27662  eulerpartgbij  27979  plymulx  28173  lgamgulmlem2  28240  lgam1  28274  faclim  28776  ptrest  29653  ovoliunnfl  29661  voliunnfl  29663  mbfposadd  29667  dvtan  29670  itg2addnclem  29671  ibladdnclem  29676  itgaddnclem1  29678  iblabsnclem  29683  itggt0cn  29692  ftc1anclem4  29698  ftc1anclem5  29699  ftc1anclem6  29700  ftc1anclem7  29701  ftc1anclem8  29702  dvcncxp1  29705  dvcnsqrt  29706  dvasin  29708  dvacos  29709  areacirclem1  29712  arearect  30816  areaquad  30817  lhe4.4ex1a  30862  itgsin0pilem1  31295  wallispilem4  31396  wallispi2  31401  stirlinglem1  31402  stirlinglem3  31404  dirkercncflem2  31432  fourierdlem48  31483  fourierdlem49  31484  fourierdlem56  31491  fourierdlem57  31492  fourierdlem58  31493  fourierdlem60  31495  fourierdlem61  31496  fourierdlem62  31497  fourierdlem107  31542  fouriersw  31560
  Copyright terms: Public domain W3C validator