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

Theorem mpteq2ia 4449
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 2428 . . 3  |-  A  =  A
21ax-gen 1663 . 2  |-  A. x  A  =  A
3 mpteq2ia.1 . . 3  |-  ( x  e.  A  ->  B  =  C )
43rgen 2724 . 2  |-  A. x  e.  A  B  =  C
5 mpteq12f 4443 . 2  |-  ( ( A. x  A  =  A  /\  A. x  e.  A  B  =  C )  ->  (
x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
62, 4, 5mp2an 676 1  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435    = wceq 1437    e. wcel 1872   A.wral 2714    |-> cmpt 4425
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-ral 2719  df-opab 4426  df-mpt 4427
This theorem is referenced by:  mpteq2i  4450  feqresmpt  5879  elfvmptrab  5931  fmptap  6046  offres  6746  resixpfo  7515  dfoi  7979  cantnflem1d  8145  cantnflem1  8146  dfceil2  12018  dfid5  13034  dfid6  13035  cnrecnv  13172  ackbijnn  13829  harmonic  13860  ege2le3  14087  eirrlem  14199  prmrec  14809  imasdsval2  15360  imasdsval2OLD  15372  cayleylem1  16996  pmtrprfval  17071  gsumzsplit  17503  gsum2dlem2  17546  dmdprdsplitlem  17613  coe1sclmul  18818  coe1sclmul2  18820  frlmip  19278  mdetunilem9  19587  leordtvallem1  20168  leordtvallem2  20169  txkgen  20609  cnmpt1st  20625  cnmpt2nd  20626  tmdgsum  21052  tsmssplit  21108  cnfldnm  21741  expcn  21846  pcorev2  22001  pi1xfrcnv  22030  rrxip  22291  mbfi1flim  22623  itg2uba  22643  itg2cnlem1  22661  itg2cnlem2  22662  itgitg2  22706  itgss3  22714  itgless  22716  ibladdlem  22719  itgaddlem1  22722  iblabslem  22727  itggt0  22741  itgcn  22742  limcdif  22773  limcres  22783  cnplimc  22784  dvcobr  22842  dvexp  22849  dveflem  22873  dvef  22874  dvlip  22887  dvlipcn  22888  lhop  22910  tdeglem2  22952  plyid  23105  coeidp  23159  dgrid  23160  pserdvlem2  23325  abelth  23338  dvrelog  23524  logcn  23534  dvlog  23538  advlog  23541  advlogexp  23542  logtayl  23547  logccv  23550  dvcxp1  23622  dvsqrt  23624  dvcncxp1  23625  dvcnsqrt  23626  resqrtcn  23631  loglesqrt  23640  logblog  23671  dvatan  23803  leibpilem2  23809  leibpi  23810  efrlim  23837  sqrtlim  23840  amgmlem  23857  emcllem5  23867  lgamgulmlem2  23897  lgam1  23931  chtublem  24081  logfacrlim2  24096  bposlem6  24159  chto1lb  24258  vmadivsum  24262  dchrvmasumlema  24280  mulogsumlem  24311  logdivsum  24313  logsqvma2  24323  log2sumbnd  24324  selberglem1  24325  selberglem3  24327  selberg  24328  selberg2lem  24330  selberg2  24331  pntrmax  24344  pntrsumo1  24345  selbergr  24348  selbergs  24354  pnt2  24393  pnt  24394  ostth2  24417  ostth  24419  hilnormi  26758  bra0  27545  partfun  28224  zrhre  28775  qqhre  28776  eulerpartgbij  29157  plymulx  29389  faclim  30333  ptrest  31846  poimirlem19  31866  poimirlem20  31867  poimirlem30  31877  ovoliunnfl  31889  voliunnfl  31891  mbfposadd  31895  dvtan  31899  itg2addnclem  31900  ibladdnclem  31905  itgaddnclem1  31907  iblabsnclem  31912  itggt0cn  31921  ftc1anclem4  31927  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anclem7  31930  ftc1anclem8  31931  dvasin  31935  dvacos  31936  areacirclem1  31939  arearect  36013  areaquad  36014  mptrcllem  36133  dfrcl2  36179  dfrcl3  36180  dftrcl3  36225  dfrtrcl3  36238  dfrtrcl4  36243  lhe4.4ex1a  36591  binomcxplemrat  36612  rnsnf  37362  dvnprodlem1  37704  itgsin0pilem1  37709  wallispilem4  37813  wallispi2  37818  stirlinglem1  37819  stirlinglem3  37821  dirkercncflem2  37849  fourierdlem48  37901  fourierdlem49  37902  fourierdlem56  37909  fourierdlem57  37910  fourierdlem58  37911  fourierdlem62  37915  fourierdlem107  37960  fouriersw  37978  etransclem46  38028  sge0tsms  38073  sge0less  38085  sge0iun  38112  meadjun  38151  ovn02  38237  hoidmv1le  38263
  Copyright terms: Public domain W3C validator