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

Theorem mpteq2ia 4566
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 2514 . . 3 𝐴 = 𝐴
21ax-gen 1700 . 2 𝑥 𝐴 = 𝐴
3 mpteq2ia.1 . . 3 (𝑥𝐴𝐵 = 𝐶)
43rgen 2810 . 2 𝑥𝐴 𝐵 = 𝐶
5 mpteq12f 4559 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
62, 4, 5mp2an 703 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472   = wceq 1474  wcel 1938  wral 2800  cmpt 4541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-ral 2805  df-opab 4542  df-mpt 4543
This theorem is referenced by:  mpteq2i  4567  feqresmpt  6049  elfvmptrab  6103  fmptap  6223  offres  6934  resixpfo  7712  dfoi  8179  cantnflem1d  8348  cantnflem1  8349  dfceil2  12374  dfid5  13478  dfid6  13479  cnrecnv  13616  ackbijnn  14272  harmonic  14303  ege2le3  14532  eirrlem  14644  prmrec  15352  imasdsval2  15890  imasdsval2OLD  15902  cayleylem1  17551  pmtrprfval  17626  gsumzsplit  18061  gsum2dlem2  18104  dmdprdsplitlem  18170  coe1sclmul  19381  coe1sclmul2  19383  frlmip  19843  mdetunilem9  20152  leordtvallem1  20731  leordtvallem2  20732  txkgen  21172  cnmpt1st  21188  cnmpt2nd  21189  tmdgsum  21616  tsmssplit  21672  cnfldnm  22305  expcn  22410  pcorev2  22563  pi1xfrcnv  22592  rrxip  22853  mbfi1flim  23175  itg2uba  23195  itg2cnlem1  23213  itg2cnlem2  23214  itgitg2  23258  itgss3  23266  itgless  23268  ibladdlem  23271  itgaddlem1  23274  iblabslem  23279  itggt0  23293  itgcn  23294  limcdif  23325  limcres  23335  cnplimc  23336  dvcobr  23394  dvexp  23401  dveflem  23425  dvef  23426  dvlip  23439  dvlipcn  23440  lhop  23462  tdeglem2  23504  plyid  23657  coeidp  23711  dgrid  23712  pserdvlem2  23877  abelth  23890  dvrelog  24074  logcn  24084  dvlog  24088  advlog  24091  advlogexp  24092  logtayl  24097  logccv  24100  dvcxp1  24172  dvsqrt  24174  dvcncxp1  24175  dvcnsqrt  24176  resqrtcn  24181  loglesqrt  24190  logblog  24221  dvatan  24353  leibpilem2  24359  leibpi  24360  efrlim  24387  sqrtlim  24390  amgmlem  24407  emcllem5  24417  lgamgulmlem2  24447  lgam1  24481  chtublem  24629  logfacrlim2  24644  bposlem6  24707  chto1lb  24860  vmadivsum  24864  dchrvmasumlema  24882  mulogsumlem  24913  logdivsum  24915  logsqvma2  24925  log2sumbnd  24926  selberglem1  24927  selberglem3  24929  selberg  24930  selberg2lem  24932  selberg2  24933  pntrmax  24946  pntrsumo1  24947  selbergr  24950  selbergs  24956  pnt2  24995  pnt  24996  ostth2  25019  ostth  25021  hilnormi  27196  bra0  27985  partfun  28650  zrhre  29191  qqhre  29192  eulerpartgbij  29572  plymulx  29800  faclim  30731  ptrest  32472  poimirlem19  32492  poimirlem20  32493  poimirlem30  32503  ovoliunnfl  32515  voliunnfl  32517  mbfposadd  32521  dvtan  32524  itg2addnclem  32525  ibladdnclem  32530  itgaddnclem1  32532  iblabsnclem  32537  itggt0cn  32546  ftc1anclem4  32552  ftc1anclem5  32553  ftc1anclem6  32554  ftc1anclem7  32555  ftc1anclem8  32556  dvasin  32560  dvacos  32561  areacirclem1  32564  arearect  36721  areaquad  36722  mptrcllem  36840  dfrcl2  36886  dfrcl3  36887  dftrcl3  36932  dfrtrcl3  36945  dfrtrcl4  36950  lhe4.4ex1a  37451  binomcxplemrat  37472  rnsnf  38267  dvnprodlem1  38743  itgsin0pilem1  38748  wallispilem4  38868  wallispi2  38873  stirlinglem1  38874  stirlinglem3  38876  dirkercncflem2  38904  fourierdlem48  38956  fourierdlem49  38957  fourierdlem56  38964  fourierdlem57  38965  fourierdlem58  38966  fourierdlem62  38970  fourierdlem107  39015  fouriersw  39033  etransclem46  39083  sge0tsms  39184  sge0less  39196  sge0iun  39223  meadjun  39266  ovn02  39369  hoidmv1le  39395  hspmbllem2  39428
  Copyright terms: Public domain W3C validator