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

Theorem mpteq2ia 4700
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 2621 . . 3 𝐴 = 𝐴
21ax-gen 1719 . 2 𝑥 𝐴 = 𝐴
3 mpteq2ia.1 . . 3 (𝑥𝐴𝐵 = 𝐶)
43rgen 2917 . 2 𝑥𝐴 𝐵 = 𝐶
5 mpteq12f 4691 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
62, 4, 5mp2an 707 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1478   = wceq 1480  wcel 1987  wral 2907  cmpt 4673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2912  df-opab 4674  df-mpt 4675
This theorem is referenced by:  mpteq2i  4701  feqresmpt  6207  elfvmptrab  6262  fmptap  6390  offres  7108  resixpfo  7890  dfoi  8360  cantnflem1d  8529  cantnflem1  8530  dfceil2  12580  dfid5  13701  dfid6  13702  cnrecnv  13839  ackbijnn  14485  harmonic  14516  ege2le3  14745  eirrlem  14857  prmrec  15550  imasdsval2  16097  cayleylem1  17753  pmtrprfval  17828  gsumzsplit  18248  gsum2dlem2  18291  dmdprdsplitlem  18357  coe1sclmul  19571  coe1sclmul2  19573  frlmip  20036  mdetunilem9  20345  leordtvallem1  20924  leordtvallem2  20925  txkgen  21365  cnmpt1st  21381  cnmpt2nd  21382  tmdgsum  21809  tsmssplit  21865  cnfldnm  22492  expcn  22583  pcorev2  22736  pi1xfrcnv  22765  rrxip  23086  mbfi1flim  23396  itg2uba  23416  itg2cnlem1  23434  itg2cnlem2  23435  itgitg2  23479  itgss3  23487  itgless  23489  ibladdlem  23492  itgaddlem1  23495  iblabslem  23500  itggt0  23514  itgcn  23515  limcdif  23546  limcres  23556  cnplimc  23557  dvcobr  23615  dvexp  23622  dveflem  23646  dvef  23647  dvlip  23660  dvlipcn  23661  lhop  23683  tdeglem2  23725  plyid  23869  coeidp  23923  dgrid  23924  pserdvlem2  24086  abelth  24099  dvrelog  24283  logcn  24293  dvlog  24297  advlog  24300  advlogexp  24301  logtayl  24306  logccv  24309  dvcxp1  24381  dvsqrt  24383  dvcncxp1  24384  dvcnsqrt  24385  resqrtcn  24390  loglesqrt  24399  logblog  24430  dvatan  24562  leibpilem2  24568  leibpi  24569  efrlim  24596  sqrtlim  24599  amgmlem  24616  emcllem5  24626  lgamgulmlem2  24656  lgam1  24690  chtublem  24836  logfacrlim2  24851  bposlem6  24914  chto1lb  25067  vmadivsum  25071  dchrvmasumlema  25089  mulogsumlem  25120  logdivsum  25122  logsqvma2  25132  log2sumbnd  25133  selberglem1  25134  selberglem3  25136  selberg  25137  selberg2lem  25139  selberg2  25140  pntrmax  25153  pntrsumo1  25154  selbergr  25157  selbergs  25163  pnt2  25202  pnt  25203  ostth2  25226  ostth  25228  hilnormi  27866  bra0  28655  partfun  29315  zrhre  29842  qqhre  29843  eulerpartgbij  30212  plymulx  30402  faclim  31337  ptrest  33037  poimirlem19  33057  poimirlem20  33058  poimirlem30  33068  ovoliunnfl  33080  voliunnfl  33082  mbfposadd  33086  dvtan  33089  itg2addnclem  33090  ibladdnclem  33095  itgaddnclem1  33097  iblabsnclem  33102  itggt0cn  33111  ftc1anclem4  33117  ftc1anclem5  33118  ftc1anclem6  33119  ftc1anclem7  33120  ftc1anclem8  33121  dvasin  33125  dvacos  33126  areacirclem1  33129  arearect  37279  areaquad  37280  mptrcllem  37398  dfrcl2  37444  dfrcl3  37445  dftrcl3  37490  dfrtrcl3  37503  dfrtrcl4  37508  lhe4.4ex1a  38007  binomcxplemrat  38028  rnsnf  38841  feqresmptf  38905  limsupresre  39329  limsupvaluzmpt  39350  dvnprodlem1  39464  itgsin0pilem1  39469  wallispilem4  39589  wallispi2  39594  stirlinglem1  39595  stirlinglem3  39597  dirkercncflem2  39625  fourierdlem48  39675  fourierdlem49  39676  fourierdlem56  39683  fourierdlem57  39684  fourierdlem58  39685  fourierdlem62  39689  fourierdlem107  39734  fouriersw  39752  etransclem46  39801  sge0tsms  39901  sge0less  39913  sge0iun  39940  meadjun  39983  ovn02  40086  hoidmv1le  40112  hspmbllem2  40145  smflimsuplem3  40332
  Copyright terms: Public domain W3C validator