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

Theorem mpteq2ia 4362
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 2433 . . 3  |-  A  =  A
21ax-gen 1594 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2771 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4356 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 665 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1360    = wceq 1362    e. wcel 1755   A.wral 2705    e. cmpt 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-opab 4339  df-mpt 4340
This theorem is referenced by:  mpteq2i  4363  feqresmpt  5733  fmptap  5888  offres  6561  resixpfo  7289  dfoi  7713  cantnflem1d  7884  cantnflem1  7885  cantnflem1dOLD  7907  cantnflem1OLD  7908  dfceil2  11664  cnrecnv  12638  ackbijnn  13274  harmonic  13304  ege2le3  13358  eirrlem  13469  prmrec  13966  imasdsval2  14437  cayleylem1  15897  pmtrprfval  15973  gsumzsplit  16398  gsumzsplitOLD  16399  gsumsn  16425  gsum2dlem2  16436  gsum2dOLD  16438  dmdprdsplitlem  16508  dmdprdsplitlemOLD  16509  coe1sclmul  17633  coe1sclmul2  17635  frlmip  18045  mdetunilem9  18268  leordtvallem1  18656  leordtvallem2  18657  txkgen  19067  cnmpt1st  19083  cnmpt2nd  19084  tmdgsum  19508  tsmssplit  19568  cnfldnm  20200  expcn  20290  pcorev2  20442  pi1xfrcnv  20471  rrxip  20736  mbfi1flim  21043  itg2uba  21063  itg2cnlem1  21081  itg2cnlem2  21082  itgitg2  21126  itgss3  21134  itgless  21136  ibladdlem  21139  itgaddlem1  21142  iblabslem  21147  itggt0  21161  itgcn  21162  limcdif  21193  limcres  21203  cnplimc  21204  dvcobr  21262  dvexp  21269  dveflem  21293  dvef  21294  dvlip  21307  dvlipcn  21308  lhop  21330  tdeglem2  21415  mdegfvalOLD  21417  plyid  21562  coeidp  21615  dgrid  21616  pserdvlem2  21778  abelth  21791  dvrelog  21967  logcn  21977  dvlog  21981  advlog  21984  advlogexp  21985  logtayl  21990  logccv  21993  dvcxp1  22065  dvsqr  22067  resqrcn  22072  loglesqr  22081  dvatan  22215  leibpilem2  22221  leibpi  22222  efrlim  22248  sqrlim  22251  amgmlem  22268  emcllem5  22278  chtublem  22435  logfacrlim2  22450  bposlem6  22513  chto1lb  22612  vmadivsum  22616  dchrvmasumlema  22634  mulogsumlem  22665  logdivsum  22667  logsqvma2  22677  log2sumbnd  22678  selberglem1  22679  selberglem3  22681  selberg  22682  selberg2lem  22684  selberg2  22685  pntrmax  22698  pntrsumo1  22699  selbergr  22702  selbergs  22708  pnt2  22747  pnt  22748  ostth2  22771  ostth  22773  hilnormi  24388  bra0  25177  partfun  25817  gsumsnf  26096  zrhre  26299  qqhre  26300  eulerpartgbij  26603  plymulx  26797  lgamgulmlem2  26864  lgam1  26898  faclim  27399  ptrest  28269  ovoliunnfl  28277  voliunnfl  28279  mbfposadd  28283  dvtan  28286  itg2addnclem  28287  ibladdnclem  28292  itgaddnclem1  28294  iblabsnclem  28299  itggt0cn  28308  ftc1anclem4  28314  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  dvcncxp1  28321  dvcnsqr  28322  dvasin  28324  dvacos  28325  areacirclem1  28328  arearect  29436  areaquad  29437  lhe4.4ex1a  29448  itgsin0pilem1  29636  wallispilem4  29709  wallispi2  29714  stirlinglem1  29715  stirlinglem3  29717  elfvmptrab  30001
  Copyright terms: Public domain W3C validator