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

Theorem mpteq2ia 3999
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 2253 . . 3  |-  A  =  A
21ax-gen 1536 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2570 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 3993 . 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 2509    e. cmpt 3974
This theorem is referenced by:  mpteq2i  4000  feqresmpt  5428  fmptap  5562  offres  5944  resixpfo  6740  dfoi  7110  cantnflem1d  7274  cantnflem1  7275  cnrecnv  11527  ackbijnn  12163  harmonic  12191  ege2le3  12245  eirrlem  12356  prmrec  12843  imasdsval2  13293  cayleylem1  14622  gsumzsplit  15041  gsumsn  15055  gsum2d  15058  dmdprdsplitlem  15107  coe1sclmul  16190  coe1sclmul2  16192  leordtvallem1  16772  leordtvallem2  16773  txkgen  17178  cnmpt1st  17194  cnmpt2nd  17195  tmdgsum  17610  tsmssplit  17666  cnfldnm  18120  expcn  18208  pcorev2  18358  pi1xfrcnv  18387  mbfi1flim  18910  itg2uba  18930  itg2cnlem1  18948  itg2cnlem2  18949  itgitg2  18993  itgss3  19001  itgless  19003  ibladdlem  19006  itgaddlem1  19009  iblabslem  19014  itggt0  19028  itgcn  19029  limcdif  19058  limcres  19068  cnplimc  19069  dvcobr  19127  dvexp  19134  dveflem  19158  dvef  19159  dvlip  19172  dvlipcn  19173  lhop  19195  tdeglem2  19279  plyid  19423  coeidp  19476  dgrid  19477  pserdvlem2  19636  abelth  19649  dvrelog  19816  logcn  19826  dvlog  19830  advlog  19833  advlogexp  19834  logtayl  19839  logccv  19842  dvcxp1  19914  dvsqr  19916  resqrcn  19921  loglesqr  19930  dvatan  20063  leibpilem2  20069  leibpi  20070  efrlim  20096  sqrlim  20099  amgmlem  20116  emcllem5  20125  chtublem  20282  logfacrlim2  20297  bposlem6  20360  chto1lb  20459  vmadivsum  20463  dchrvmasumlema  20481  mulogsumlem  20512  logdivsum  20514  logsqvma2  20524  log2sumbnd  20525  selberglem1  20526  selberglem3  20528  selberg  20529  selberg2lem  20531  selberg2  20532  pntrmax  20545  pntrsumo1  20546  selbergr  20549  selbergs  20555  pnt2  20594  pnt  20595  ostth2  20618  ostth  20620  hilnormi  21572  bra0  22360  svs2  24653  svs3  24654  lhe4.4ex1a  26712
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 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-ral 2513  df-opab 3975  df-mpt 3976
  Copyright terms: Public domain W3C validator