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

Theorem mpteq2ia 4662
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Hypothesis
Ref Expression
mpteq2ia.1 (𝑥𝐴𝐵 = 𝐶)
Assertion
Ref Expression
mpteq2ia (𝑥𝐴𝐵) = (𝑥𝐴𝐶)

Proof of Theorem mpteq2ia
StepHypRef Expression
1 eqid 2609 . . 3 𝐴 = 𝐴
21ax-gen 1712 . 2 𝑥 𝐴 = 𝐴
3 mpteq2ia.1 . . 3 (𝑥𝐴𝐵 = 𝐶)
43rgen 2905 . 2 𝑥𝐴 𝐵 = 𝐶
5 mpteq12f 4655 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
62, 4, 5mp2an 703 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472   = wceq 1474  wcel 1976  wral 2895  cmpt 4637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-ral 2900  df-opab 4638  df-mpt 4639
This theorem is referenced by:  mpteq2i  4663  feqresmpt  6145  elfvmptrab  6199  fmptap  6319  offres  7031  resixpfo  7809  dfoi  8276  cantnflem1d  8445  cantnflem1  8446  dfceil2  12457  dfid5  13561  dfid6  13562  cnrecnv  13699  ackbijnn  14345  harmonic  14376  ege2le3  14605  eirrlem  14717  prmrec  15410  imasdsval2  15945  cayleylem1  17601  pmtrprfval  17676  gsumzsplit  18096  gsum2dlem2  18139  dmdprdsplitlem  18205  coe1sclmul  19419  coe1sclmul2  19421  frlmip  19878  mdetunilem9  20187  leordtvallem1  20766  leordtvallem2  20767  txkgen  21207  cnmpt1st  21223  cnmpt2nd  21224  tmdgsum  21651  tsmssplit  21707  cnfldnm  22324  expcn  22414  pcorev2  22567  pi1xfrcnv  22596  rrxip  22903  mbfi1flim  23213  itg2uba  23233  itg2cnlem1  23251  itg2cnlem2  23252  itgitg2  23296  itgss3  23304  itgless  23306  ibladdlem  23309  itgaddlem1  23312  iblabslem  23317  itggt0  23331  itgcn  23332  limcdif  23363  limcres  23373  cnplimc  23374  dvcobr  23432  dvexp  23439  dveflem  23463  dvef  23464  dvlip  23477  dvlipcn  23478  lhop  23500  tdeglem2  23542  plyid  23686  coeidp  23740  dgrid  23741  pserdvlem2  23903  abelth  23916  dvrelog  24100  logcn  24110  dvlog  24114  advlog  24117  advlogexp  24118  logtayl  24123  logccv  24126  dvcxp1  24198  dvsqrt  24200  dvcncxp1  24201  dvcnsqrt  24202  resqrtcn  24207  loglesqrt  24216  logblog  24247  dvatan  24379  leibpilem2  24385  leibpi  24386  efrlim  24413  sqrtlim  24416  amgmlem  24433  emcllem5  24443  lgamgulmlem2  24473  lgam1  24507  chtublem  24653  logfacrlim2  24668  bposlem6  24731  chto1lb  24884  vmadivsum  24888  dchrvmasumlema  24906  mulogsumlem  24937  logdivsum  24939  logsqvma2  24949  log2sumbnd  24950  selberglem1  24951  selberglem3  24953  selberg  24954  selberg2lem  24956  selberg2  24957  pntrmax  24970  pntrsumo1  24971  selbergr  24974  selbergs  24980  pnt2  25019  pnt  25020  ostth2  25043  ostth  25045  hilnormi  27210  bra0  27999  partfun  28664  zrhre  29197  qqhre  29198  eulerpartgbij  29567  plymulx  29757  faclim  30691  ptrest  32374  poimirlem19  32394  poimirlem20  32395  poimirlem30  32405  ovoliunnfl  32417  voliunnfl  32419  mbfposadd  32423  dvtan  32426  itg2addnclem  32427  ibladdnclem  32432  itgaddnclem1  32434  iblabsnclem  32439  itggt0cn  32448  ftc1anclem4  32454  ftc1anclem5  32455  ftc1anclem6  32456  ftc1anclem7  32457  ftc1anclem8  32458  dvasin  32462  dvacos  32463  areacirclem1  32466  arearect  36616  areaquad  36617  mptrcllem  36735  dfrcl2  36781  dfrcl3  36782  dftrcl3  36827  dfrtrcl3  36840  dfrtrcl4  36845  lhe4.4ex1a  37346  binomcxplemrat  37367  rnsnf  38161  dvnprodlem1  38633  itgsin0pilem1  38638  wallispilem4  38758  wallispi2  38763  stirlinglem1  38764  stirlinglem3  38766  dirkercncflem2  38794  fourierdlem48  38844  fourierdlem49  38845  fourierdlem56  38852  fourierdlem57  38853  fourierdlem58  38854  fourierdlem62  38858  fourierdlem107  38903  fouriersw  38921  etransclem46  38970  sge0tsms  39070  sge0less  39082  sge0iun  39109  meadjun  39152  ovn02  39255  hoidmv1le  39281  hspmbllem2  39314
  Copyright terms: Public domain W3C validator