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

Theorem mpteq2ia 4076
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 2258 . . 3  |-  A  =  A
21ax-gen 1536 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2583 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4070 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 656 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532    = wceq 1619    e. wcel 1621   A.wral 2518    e. cmpt 4051
This theorem is referenced by:  mpteq2i  4077  feqresmpt  5510  fmptap  5644  offres  6026  resixpfo  6822  dfoi  7194  cantnflem1d  7358  cantnflem1  7359  cnrecnv  11615  ackbijnn  12251  harmonic  12279  ege2le3  12333  eirrlem  12444  prmrec  12931  imasdsval2  13381  cayleylem1  14749  gsumzsplit  15168  gsumsn  15182  gsum2d  15185  dmdprdsplitlem  15234  coe1sclmul  16320  coe1sclmul2  16322  leordtvallem1  16902  leordtvallem2  16903  txkgen  17308  cnmpt1st  17324  cnmpt2nd  17325  tmdgsum  17740  tsmssplit  17796  cnfldnm  18250  expcn  18338  pcorev2  18488  pi1xfrcnv  18517  mbfi1flim  19040  itg2uba  19060  itg2cnlem1  19078  itg2cnlem2  19079  itgitg2  19123  itgss3  19131  itgless  19133  ibladdlem  19136  itgaddlem1  19139  iblabslem  19144  itggt0  19158  itgcn  19159  limcdif  19188  limcres  19198  cnplimc  19199  dvcobr  19257  dvexp  19264  dveflem  19288  dvef  19289  dvlip  19302  dvlipcn  19303  lhop  19325  tdeglem2  19409  plyid  19553  coeidp  19606  dgrid  19607  pserdvlem2  19766  abelth  19779  dvrelog  19946  logcn  19956  dvlog  19960  advlog  19963  advlogexp  19964  logtayl  19969  logccv  19972  dvcxp1  20044  dvsqr  20046  resqrcn  20051  loglesqr  20060  dvatan  20193  leibpilem2  20199  leibpi  20200  efrlim  20226  sqrlim  20229  amgmlem  20246  emcllem5  20255  chtublem  20412  logfacrlim2  20427  bposlem6  20490  chto1lb  20589  vmadivsum  20593  dchrvmasumlema  20611  mulogsumlem  20642  logdivsum  20644  logsqvma2  20654  log2sumbnd  20655  selberglem1  20656  selberglem3  20658  selberg  20659  selberg2lem  20661  selberg2  20662  pntrmax  20675  pntrsumo1  20676  selbergr  20679  selbergs  20685  pnt2  20724  pnt  20725  ostth2  20748  ostth  20750  hilnormi  21702  bra0  22490  svs2  24854  svs3  24855  lhe4.4ex1a  26913
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-ral 2523  df-opab 4052  df-mpt 4053
  Copyright terms: Public domain W3C validator