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

Theorem mpteq2ia 4395
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 1591 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2802 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4389 . 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 1367    = wceq 1369    e. wcel 1756   A.wral 2736    e. cmpt 4371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-ral 2741  df-opab 4372  df-mpt 4373
This theorem is referenced by:  mpteq2i  4396  feqresmpt  5766  fmptap  5922  offres  6593  resixpfo  7322  dfoi  7746  cantnflem1d  7917  cantnflem1  7918  cantnflem1dOLD  7940  cantnflem1OLD  7941  dfceil2  11701  cnrecnv  12675  ackbijnn  13312  harmonic  13342  ege2le3  13396  eirrlem  13507  prmrec  14004  imasdsval2  14475  cayleylem1  15938  pmtrprfval  16014  gsumzsplit  16439  gsumzsplitOLD  16440  gsumsn  16471  gsum2dlem2  16484  gsum2dOLD  16486  dmdprdsplitlem  16556  dmdprdsplitlemOLD  16557  coe1sclmul  17757  coe1sclmul2  17759  frlmip  18225  mdetunilem9  18448  leordtvallem1  18836  leordtvallem2  18837  txkgen  19247  cnmpt1st  19263  cnmpt2nd  19264  tmdgsum  19688  tsmssplit  19748  cnfldnm  20380  expcn  20470  pcorev2  20622  pi1xfrcnv  20651  rrxip  20916  mbfi1flim  21223  itg2uba  21243  itg2cnlem1  21261  itg2cnlem2  21262  itgitg2  21306  itgss3  21314  itgless  21316  ibladdlem  21319  itgaddlem1  21322  iblabslem  21327  itggt0  21341  itgcn  21342  limcdif  21373  limcres  21383  cnplimc  21384  dvcobr  21442  dvexp  21449  dveflem  21473  dvef  21474  dvlip  21487  dvlipcn  21488  lhop  21510  tdeglem2  21552  mdegfvalOLD  21554  plyid  21699  coeidp  21752  dgrid  21753  pserdvlem2  21915  abelth  21928  dvrelog  22104  logcn  22114  dvlog  22118  advlog  22121  advlogexp  22122  logtayl  22127  logccv  22130  dvcxp1  22202  dvsqr  22204  resqrcn  22209  loglesqr  22218  dvatan  22352  leibpilem2  22358  leibpi  22359  efrlim  22385  sqrlim  22388  amgmlem  22405  emcllem5  22415  chtublem  22572  logfacrlim2  22587  bposlem6  22650  chto1lb  22749  vmadivsum  22753  dchrvmasumlema  22771  mulogsumlem  22802  logdivsum  22804  logsqvma2  22814  log2sumbnd  22815  selberglem1  22816  selberglem3  22818  selberg  22819  selberg2lem  22821  selberg2  22822  pntrmax  22835  pntrsumo1  22836  selbergr  22839  selbergs  22845  pnt2  22884  pnt  22885  ostth2  22908  ostth  22910  hilnormi  24587  bra0  25376  partfun  26015  gsumsnf  26266  zrhre  26467  qqhre  26468  eulerpartgbij  26777  plymulx  26971  lgamgulmlem2  27038  lgam1  27072  faclim  27574  ptrest  28451  ovoliunnfl  28459  voliunnfl  28461  mbfposadd  28465  dvtan  28468  itg2addnclem  28469  ibladdnclem  28474  itgaddnclem1  28476  iblabsnclem  28481  itggt0cn  28490  ftc1anclem4  28496  ftc1anclem5  28497  ftc1anclem6  28498  ftc1anclem7  28499  ftc1anclem8  28500  dvcncxp1  28503  dvcnsqr  28504  dvasin  28506  dvacos  28507  areacirclem1  28510  arearect  29617  areaquad  29618  lhe4.4ex1a  29629  itgsin0pilem1  29816  wallispilem4  29889  wallispi2  29894  stirlinglem1  29895  stirlinglem3  29897  elfvmptrab  30181  mp2pm2mp  31136
  Copyright terms: Public domain W3C validator