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

Theorem mpteq2ia 4118
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 2296 . . 3  |-  A  =  A
21ax-gen 1536 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2621 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4112 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 653 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    = wceq 1632    e. wcel 1696   A.wral 2556    e. cmpt 4093
This theorem is referenced by:  mpteq2i  4119  feqresmpt  5592  fmptap  5726  offres  6108  resixpfo  6870  dfoi  7242  cantnflem1d  7406  cantnflem1  7407  cnrecnv  11666  ackbijnn  12302  harmonic  12333  ege2le3  12387  eirrlem  12498  prmrec  12985  imasdsval2  13435  cayleylem1  14803  gsumzsplit  15222  gsumsn  15236  gsum2d  15239  dmdprdsplitlem  15288  coe1sclmul  16374  coe1sclmul2  16376  leordtvallem1  16956  leordtvallem2  16957  txkgen  17362  cnmpt1st  17378  cnmpt2nd  17379  tmdgsum  17794  tsmssplit  17850  cnfldnm  18304  expcn  18392  pcorev2  18542  pi1xfrcnv  18571  mbfi1flim  19094  itg2uba  19114  itg2cnlem1  19132  itg2cnlem2  19133  itgitg2  19177  itgss3  19185  itgless  19187  ibladdlem  19190  itgaddlem1  19193  iblabslem  19198  itggt0  19212  itgcn  19213  limcdif  19242  limcres  19252  cnplimc  19253  dvcobr  19311  dvexp  19318  dveflem  19342  dvef  19343  dvlip  19356  dvlipcn  19357  lhop  19379  tdeglem2  19463  plyid  19607  coeidp  19660  dgrid  19661  pserdvlem2  19820  abelth  19833  dvrelog  20000  logcn  20010  dvlog  20014  advlog  20017  advlogexp  20018  logtayl  20023  logccv  20026  dvcxp1  20098  dvsqr  20100  resqrcn  20105  loglesqr  20114  dvatan  20247  leibpilem2  20253  leibpi  20254  efrlim  20280  sqrlim  20283  amgmlem  20300  emcllem5  20309  chtublem  20466  logfacrlim2  20481  bposlem6  20544  chto1lb  20643  vmadivsum  20647  dchrvmasumlema  20665  mulogsumlem  20696  logdivsum  20698  logsqvma2  20708  log2sumbnd  20709  selberglem1  20710  selberglem3  20712  selberg  20713  selberg2lem  20715  selberg2  20716  pntrmax  20729  pntrsumo1  20730  selbergr  20733  selbergs  20739  pnt2  20778  pnt  20779  ostth2  20802  ostth  20804  hilnormi  21758  bra0  22546  partfun  23255  faclimlem3  24119  ovoliunnfl  25001  itg2addnclem  25003  ibladdnclem  25007  itgaddnclem1  25009  iblabsnclem  25014  itggt0cn  25023  dvreasin  25026  dvreacos  25027  areacirclem2  25028  svs2  25590  svs3  25591  lhe4.4ex1a  27649  itgsin0pilem1  27847  wallispilem4  27920  wallispi2  27925  stirlinglem1  27926  stirlinglem3  27928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-opab 4094  df-mpt 4095
  Copyright terms: Public domain W3C validator