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

Theorem mpteq2ia 4498
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 2461 . . 3  |-  A  =  A
21ax-gen 1679 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2758 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4492 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 683 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1452    = wceq 1454    e. wcel 1897   A.wral 2748    |-> cmpt 4474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-ral 2753  df-opab 4475  df-mpt 4476
This theorem is referenced by:  mpteq2i  4499  feqresmpt  5941  elfvmptrab  5993  fmptap  6110  offres  6814  resixpfo  7585  dfoi  8051  cantnflem1d  8218  cantnflem1  8219  dfceil2  12099  dfid5  13138  dfid6  13139  cnrecnv  13276  ackbijnn  13934  harmonic  13965  ege2le3  14192  eirrlem  14304  prmrec  14914  imasdsval2  15465  imasdsval2OLD  15477  cayleylem1  17101  pmtrprfval  17176  gsumzsplit  17608  gsum2dlem2  17651  dmdprdsplitlem  17718  coe1sclmul  18923  coe1sclmul2  18925  frlmip  19384  mdetunilem9  19693  leordtvallem1  20274  leordtvallem2  20275  txkgen  20715  cnmpt1st  20731  cnmpt2nd  20732  tmdgsum  21158  tsmssplit  21214  cnfldnm  21847  expcn  21952  pcorev2  22107  pi1xfrcnv  22136  rrxip  22397  mbfi1flim  22729  itg2uba  22749  itg2cnlem1  22767  itg2cnlem2  22768  itgitg2  22812  itgss3  22820  itgless  22822  ibladdlem  22825  itgaddlem1  22828  iblabslem  22833  itggt0  22847  itgcn  22848  limcdif  22879  limcres  22889  cnplimc  22890  dvcobr  22948  dvexp  22955  dveflem  22979  dvef  22980  dvlip  22993  dvlipcn  22994  lhop  23016  tdeglem2  23058  plyid  23211  coeidp  23265  dgrid  23266  pserdvlem2  23431  abelth  23444  dvrelog  23630  logcn  23640  dvlog  23644  advlog  23647  advlogexp  23648  logtayl  23653  logccv  23656  dvcxp1  23728  dvsqrt  23730  dvcncxp1  23731  dvcnsqrt  23732  resqrtcn  23737  loglesqrt  23746  logblog  23777  dvatan  23909  leibpilem2  23915  leibpi  23916  efrlim  23943  sqrtlim  23946  amgmlem  23963  emcllem5  23973  lgamgulmlem2  24003  lgam1  24037  chtublem  24187  logfacrlim2  24202  bposlem6  24265  chto1lb  24364  vmadivsum  24368  dchrvmasumlema  24386  mulogsumlem  24417  logdivsum  24419  logsqvma2  24429  log2sumbnd  24430  selberglem1  24431  selberglem3  24433  selberg  24434  selberg2lem  24436  selberg2  24437  pntrmax  24450  pntrsumo1  24451  selbergr  24454  selbergs  24460  pnt2  24499  pnt  24500  ostth2  24523  ostth  24525  hilnormi  26864  bra0  27651  partfun  28326  zrhre  28871  qqhre  28872  eulerpartgbij  29253  plymulx  29485  faclim  30430  ptrest  31983  poimirlem19  32003  poimirlem20  32004  poimirlem30  32014  ovoliunnfl  32026  voliunnfl  32028  mbfposadd  32032  dvtan  32036  itg2addnclem  32037  ibladdnclem  32042  itgaddnclem1  32044  iblabsnclem  32049  itggt0cn  32058  ftc1anclem4  32064  ftc1anclem5  32065  ftc1anclem6  32066  ftc1anclem7  32067  ftc1anclem8  32068  dvasin  32072  dvacos  32073  areacirclem1  32076  arearect  36144  areaquad  36145  mptrcllem  36264  dfrcl2  36310  dfrcl3  36311  dftrcl3  36356  dfrtrcl3  36369  dfrtrcl4  36374  lhe4.4ex1a  36721  binomcxplemrat  36742  rnsnf  37495  dvnprodlem1  37858  itgsin0pilem1  37863  wallispilem4  37967  wallispi2  37972  stirlinglem1  37973  stirlinglem3  37975  dirkercncflem2  38003  fourierdlem48  38055  fourierdlem49  38056  fourierdlem56  38063  fourierdlem57  38064  fourierdlem58  38065  fourierdlem62  38069  fourierdlem107  38114  fouriersw  38132  etransclem46  38182  sge0tsms  38259  sge0less  38271  sge0iun  38298  meadjun  38337  ovn02  38427  hoidmv1le  38453  hspmbllem2  38486
  Copyright terms: Public domain W3C validator