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

Theorem mpteq2ia 4519
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 2443 . . 3  |-  A  =  A
21ax-gen 1605 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2803 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4513 . 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 1381    = wceq 1383    e. wcel 1804   A.wral 2793    |-> cmpt 4495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-opab 4496  df-mpt 4497
This theorem is referenced by:  mpteq2i  4520  feqresmpt  5912  elfvmptrab  5962  fmptap  6079  offres  6780  resixpfo  7509  dfoi  7939  cantnflem1d  8110  cantnflem1  8111  cantnflem1dOLD  8133  cantnflem1OLD  8134  dfceil2  11950  cnrecnv  12980  ackbijnn  13622  harmonic  13652  ege2le3  13807  eirrlem  13919  prmrec  14422  imasdsval2  14895  cayleylem1  16416  pmtrprfval  16491  gsumzsplit  16923  gsumzsplitOLD  16924  gsum2dlem2  16977  gsum2dOLD  16979  dmdprdsplitlem  17063  dmdprdsplitlemOLD  17064  coe1sclmul  18302  coe1sclmul2  18304  frlmip  18787  mdetunilem9  19100  leordtvallem1  19689  leordtvallem2  19690  txkgen  20131  cnmpt1st  20147  cnmpt2nd  20148  tmdgsum  20572  tsmssplit  20632  cnfldnm  21264  expcn  21354  pcorev2  21506  pi1xfrcnv  21535  rrxip  21800  mbfi1flim  22108  itg2uba  22128  itg2cnlem1  22146  itg2cnlem2  22147  itgitg2  22191  itgss3  22199  itgless  22201  ibladdlem  22204  itgaddlem1  22207  iblabslem  22212  itggt0  22226  itgcn  22227  limcdif  22258  limcres  22268  cnplimc  22269  dvcobr  22327  dvexp  22334  dveflem  22358  dvef  22359  dvlip  22372  dvlipcn  22373  lhop  22395  tdeglem2  22437  mdegfvalOLD  22439  plyid  22584  coeidp  22638  dgrid  22639  pserdvlem2  22801  abelth  22814  dvrelog  22996  logcn  23006  dvlog  23010  advlog  23013  advlogexp  23014  logtayl  23019  logccv  23022  dvcxp1  23094  dvsqrt  23096  resqrtcn  23101  loglesqrt  23110  dvatan  23244  leibpilem2  23250  leibpi  23251  efrlim  23277  sqrtlim  23280  amgmlem  23297  emcllem5  23307  chtublem  23464  logfacrlim2  23479  bposlem6  23542  chto1lb  23641  vmadivsum  23645  dchrvmasumlema  23663  mulogsumlem  23694  logdivsum  23696  logsqvma2  23706  log2sumbnd  23707  selberglem1  23708  selberglem3  23710  selberg  23711  selberg2lem  23713  selberg2  23714  pntrmax  23727  pntrsumo1  23728  selbergr  23731  selbergs  23737  pnt2  23776  pnt  23777  ostth2  23800  ostth  23802  hilnormi  26058  bra0  26847  partfun  27494  zrhre  27975  qqhre  27976  eulerpartgbij  28289  plymulx  28483  lgamgulmlem2  28550  lgam1  28584  faclim  29147  ptrest  30024  ovoliunnfl  30032  voliunnfl  30034  mbfposadd  30038  dvtan  30041  itg2addnclem  30042  ibladdnclem  30047  itgaddnclem1  30049  iblabsnclem  30054  itggt0cn  30063  ftc1anclem4  30069  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  dvcncxp1  30076  dvcnsqrt  30077  dvasin  30079  dvacos  30080  areacirclem1  30083  arearect  31159  areaquad  31160  lhe4.4ex1a  31210  dvnprodlem1  31697  itgsin0pilem1  31702  wallispilem4  31804  wallispi2  31809  stirlinglem1  31810  stirlinglem3  31812  dirkercncflem2  31840  fourierdlem48  31891  fourierdlem49  31892  fourierdlem56  31899  fourierdlem57  31900  fourierdlem58  31901  fourierdlem62  31905  fourierdlem107  31950  fouriersw  31968  etransclem46  32017
  Copyright terms: Public domain W3C validator