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

Theorem mpteq2ia 4521
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 2454 . . 3  |-  A  =  A
21ax-gen 1623 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2814 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4515 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 670 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1396    = wceq 1398    e. wcel 1823   A.wral 2804    |-> cmpt 4497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2809  df-opab 4498  df-mpt 4499
This theorem is referenced by:  mpteq2i  4522  feqresmpt  5902  elfvmptrab  5953  fmptap  6070  offres  6768  resixpfo  7500  dfoi  7928  cantnflem1d  8098  cantnflem1  8099  cantnflem1dOLD  8121  cantnflem1OLD  8122  dfceil2  11950  cnrecnv  13083  ackbijnn  13725  harmonic  13755  ege2le3  13910  eirrlem  14022  prmrec  14527  imasdsval2  15008  cayleylem1  16639  pmtrprfval  16714  gsumzsplit  17146  gsumzsplitOLD  17147  gsum2dlem2  17197  gsum2dOLD  17199  dmdprdsplitlem  17282  dmdprdsplitlemOLD  17283  coe1sclmul  18521  coe1sclmul2  18523  frlmip  18983  mdetunilem9  19292  leordtvallem1  19881  leordtvallem2  19882  txkgen  20322  cnmpt1st  20338  cnmpt2nd  20339  tmdgsum  20763  tsmssplit  20823  cnfldnm  21455  expcn  21545  pcorev2  21697  pi1xfrcnv  21726  rrxip  21991  mbfi1flim  22299  itg2uba  22319  itg2cnlem1  22337  itg2cnlem2  22338  itgitg2  22382  itgss3  22390  itgless  22392  ibladdlem  22395  itgaddlem1  22398  iblabslem  22403  itggt0  22417  itgcn  22418  limcdif  22449  limcres  22459  cnplimc  22460  dvcobr  22518  dvexp  22525  dveflem  22549  dvef  22550  dvlip  22563  dvlipcn  22564  lhop  22586  tdeglem2  22628  mdegfvalOLD  22630  plyid  22775  coeidp  22829  dgrid  22830  pserdvlem2  22992  abelth  23005  dvrelog  23189  logcn  23199  dvlog  23203  advlog  23206  advlogexp  23207  logtayl  23212  logccv  23215  dvcxp1  23287  dvsqrt  23289  resqrtcn  23294  loglesqrt  23303  logblog  23334  dvatan  23466  leibpilem2  23472  leibpi  23473  efrlim  23500  sqrtlim  23503  amgmlem  23520  emcllem5  23530  chtublem  23687  logfacrlim2  23702  bposlem6  23765  chto1lb  23864  vmadivsum  23868  dchrvmasumlema  23886  mulogsumlem  23917  logdivsum  23919  logsqvma2  23929  log2sumbnd  23930  selberglem1  23931  selberglem3  23933  selberg  23934  selberg2lem  23936  selberg2  23937  pntrmax  23950  pntrsumo1  23951  selbergr  23954  selbergs  23960  pnt2  23999  pnt  24000  ostth2  24023  ostth  24025  hilnormi  26281  bra0  27070  partfun  27747  zrhre  28234  qqhre  28235  eulerpartgbij  28578  plymulx  28772  lgamgulmlem2  28839  lgam1  28873  faclim  29415  ptrest  30291  ovoliunnfl  30299  voliunnfl  30301  mbfposadd  30305  dvtan  30308  itg2addnclem  30309  ibladdnclem  30314  itgaddnclem1  30316  iblabsnclem  30321  itggt0cn  30330  ftc1anclem4  30336  ftc1anclem5  30337  ftc1anclem6  30338  ftc1anclem7  30339  ftc1anclem8  30340  dvcncxp1  30343  dvcnsqrt  30344  dvasin  30346  dvacos  30347  areacirclem1  30350  arearect  31427  areaquad  31428  lhe4.4ex1a  31478  binomcxplemrat  31499  dvnprodlem1  31985  itgsin0pilem1  31990  wallispilem4  32092  wallispi2  32097  stirlinglem1  32098  stirlinglem3  32100  dirkercncflem2  32128  fourierdlem48  32179  fourierdlem49  32180  fourierdlem56  32187  fourierdlem57  32188  fourierdlem58  32189  fourierdlem62  32193  fourierdlem107  32238  fouriersw  32256  etransclem46  32305  dfrcl2  38214  dfrcl3  38215  dfid5  38216  dfid6  38217  dftrcl3  38234  dfrtrcl3  38235  dfrtrcl4  38236
  Copyright terms: Public domain W3C validator