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

Theorem mpteq2ia 4884
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 2752 . . 3 𝐴 = 𝐴
21ax-gen 1863 . 2 𝑥 𝐴 = 𝐴
3 mpteq2ia.1 . . 3 (𝑥𝐴𝐵 = 𝐶)
43rgen 3052 . 2 𝑥𝐴 𝐵 = 𝐶
5 mpteq12f 4875 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
62, 4, 5mp2an 710 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1622   = wceq 1624  wcel 2131  wral 3042  cmpt 4873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-ral 3047  df-opab 4857  df-mpt 4874
This theorem is referenced by:  mpteq2i  4885  feqresmpt  6404  elfvmptrab  6460  fmptap  6592  offres  7320  resixpfo  8104  dfoi  8573  cantnflem1d  8750  cantnflem1  8751  dfceil2  12826  dfid5  13958  dfid6  13959  cnrecnv  14096  ackbijnn  14751  harmonic  14782  ege2le3  15011  eirrlem  15123  prmrec  15820  imasdsval2  16370  cayleylem1  18024  pmtrprfval  18099  gsumzsplit  18519  gsum2dlem2  18562  dmdprdsplitlem  18628  coe1sclmul  19846  coe1sclmul2  19848  frlmip  20311  mdetunilem9  20620  leordtvallem1  21208  leordtvallem2  21209  txkgen  21649  cnmpt1st  21665  cnmpt2nd  21666  tmdgsum  22092  tsmssplit  22148  cnfldnm  22775  expcn  22868  pcorev2  23020  pi1xfrcnv  23049  rrxip  23370  mbfi1flim  23681  itg2uba  23701  itg2cnlem1  23719  itg2cnlem2  23720  itgitg2  23764  itgss3  23772  itgless  23774  ibladdlem  23777  itgaddlem1  23780  iblabslem  23785  itggt0  23799  itgcn  23800  limcdif  23831  limcres  23841  cnplimc  23842  dvcobr  23900  dvexp  23907  dveflem  23933  dvef  23934  dvlip  23947  dvlipcn  23948  lhop  23970  tdeglem2  24012  plyid  24156  coeidp  24210  dgrid  24211  pserdvlem2  24373  abelth  24386  dvrelog  24574  logcn  24584  dvlog  24588  advlog  24591  advlogexp  24592  logtayl  24597  logccv  24600  dvcxp1  24672  dvsqrt  24674  dvcncxp1  24675  dvcnsqrt  24676  resqrtcn  24681  loglesqrt  24690  logblog  24721  dvatan  24853  leibpilem2  24859  leibpi  24860  efrlim  24887  sqrtlim  24890  amgmlem  24907  emcllem5  24917  lgamgulmlem2  24947  lgam1  24981  chtublem  25127  logfacrlim2  25142  bposlem6  25205  chto1lb  25358  vmadivsum  25362  dchrvmasumlema  25380  mulogsumlem  25411  logdivsum  25413  logsqvma2  25423  log2sumbnd  25424  selberglem1  25425  selberglem3  25427  selberg  25428  selberg2lem  25430  selberg2  25431  pntrmax  25444  pntrsumo1  25445  selbergr  25448  selbergs  25454  pnt2  25493  pnt  25494  ostth2  25517  ostth  25519  hilnormi  28321  bra0  29110  partfun  29776  zrhre  30364  qqhre  30365  eulerpartgbij  30735  plymulx  30926  faclim  31931  ptrest  33713  poimirlem19  33733  poimirlem20  33734  poimirlem30  33744  ovoliunnfl  33756  voliunnfl  33758  mbfposadd  33762  dvtan  33765  itg2addnclem  33766  ibladdnclem  33771  itgaddnclem1  33773  iblabsnclem  33778  itggt0cn  33787  ftc1anclem4  33793  ftc1anclem5  33794  ftc1anclem6  33795  ftc1anclem7  33796  ftc1anclem8  33797  dvasin  33801  dvacos  33802  areacirclem1  33805  arearect  38295  areaquad  38296  mptrcllem  38414  dfrcl2  38460  dfrcl3  38461  dftrcl3  38506  dfrtrcl3  38519  dfrtrcl4  38524  lhe4.4ex1a  39022  binomcxplemrat  39043  rnsnf  39861  feqresmptf  39924  limsupresre  40423  limsupvaluzmpt  40444  limsup10ex  40500  liminf10ex  40501  dvnprodlem1  40656  itgsin0pilem1  40660  wallispilem4  40780  wallispi2  40785  stirlinglem1  40786  stirlinglem3  40788  dirkercncflem2  40816  fourierdlem48  40866  fourierdlem49  40867  fourierdlem56  40874  fourierdlem57  40875  fourierdlem58  40876  fourierdlem62  40880  fourierdlem107  40925  fouriersw  40943  etransclem46  40992  sge0tsms  41092  sge0less  41104  sge0iun  41131  meadjun  41174  ovn02  41280  hoidmv1le  41306  hspmbllem2  41339  smflimsuplem3  41526
  Copyright terms: Public domain W3C validator