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

Theorem mpteq2ia 4875
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 2771 . . 3 𝐴 = 𝐴
21ax-gen 1870 . 2 𝑥 𝐴 = 𝐴
3 mpteq2ia.1 . . 3 (𝑥𝐴𝐵 = 𝐶)
43rgen 3071 . 2 𝑥𝐴 𝐵 = 𝐶
5 mpteq12f 4866 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
62, 4, 5mp2an 666 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1629   = wceq 1631  wcel 2145  wral 3061  cmpt 4864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-ral 3066  df-opab 4848  df-mpt 4865
This theorem is referenced by:  mpteq2i  4876  feqresmpt  6393  elfvmptrab  6449  fmptap  6581  offres  7311  resixpfo  8101  dfoi  8573  cantnflem1d  8750  cantnflem1  8751  dfceil2  12849  dfid5  13976  dfid6  13977  cnrecnv  14114  ackbijnn  14768  harmonic  14799  ege2le3  15027  eirrlem  15139  prmrec  15834  imasdsval2  16385  cayleylem1  18040  pmtrprfval  18115  gsumzsplit  18535  gsum2dlem2  18578  dmdprdsplitlem  18645  coe1sclmul  19868  coe1sclmul2  19870  frlmip  20335  mdetunilem9  20645  leordtvallem1  21236  leordtvallem2  21237  txkgen  21677  cnmpt1st  21693  cnmpt2nd  21694  tmdgsum  22120  tsmssplit  22176  cnfldnm  22803  expcn  22896  pcorev2  23048  pi1xfrcnv  23077  rrxip  23398  mbfi1flim  23711  itg2uba  23731  itg2cnlem1  23749  itg2cnlem2  23750  itgitg2  23794  itgss3  23802  itgless  23804  ibladdlem  23807  itgaddlem1  23810  iblabslem  23815  itggt0  23829  itgcn  23830  limcdif  23861  limcres  23871  cnplimc  23872  dvcobr  23930  dvexp  23937  dveflem  23963  dvef  23964  dvlip  23977  dvlipcn  23978  lhop  24000  tdeglem2  24042  plyid  24186  coeidp  24240  dgrid  24241  pserdvlem2  24403  abelth  24416  dvrelog  24605  logcn  24615  dvlog  24619  advlog  24622  advlogexp  24623  logtayl  24628  logccv  24631  dvcxp1  24703  dvsqrt  24705  dvcncxp1  24706  dvcnsqrt  24707  resqrtcn  24712  loglesqrt  24721  logblog  24752  dvatan  24884  leibpilem2  24890  leibpi  24891  efrlim  24918  sqrtlim  24921  amgmlem  24938  emcllem5  24948  lgamgulmlem2  24978  lgam1  25012  chtublem  25158  logfacrlim2  25173  bposlem6  25236  chto1lb  25389  vmadivsum  25393  dchrvmasumlema  25411  mulogsumlem  25442  logdivsum  25444  logsqvma2  25454  log2sumbnd  25455  selberglem1  25456  selberglem3  25458  selberg  25459  selberg2lem  25461  selberg2  25462  pntrmax  25475  pntrsumo1  25476  selbergr  25479  selbergs  25485  pnt2  25524  pnt  25525  ostth2  25548  ostth  25550  hilnormi  28361  bra0  29150  partfun  29816  zrhre  30404  qqhre  30405  eulerpartgbij  30775  plymulx  30966  faclim  31971  ptrest  33742  poimirlem19  33762  poimirlem20  33763  poimirlem30  33773  ovoliunnfl  33785  voliunnfl  33787  mbfposadd  33790  dvtan  33793  itg2addnclem  33794  ibladdnclem  33799  itgaddnclem1  33801  iblabsnclem  33806  itggt0cn  33815  ftc1anclem4  33821  ftc1anclem5  33822  ftc1anclem6  33823  ftc1anclem7  33824  ftc1anclem8  33825  dvasin  33829  dvacos  33830  areacirclem1  33833  arearect  38328  areaquad  38329  mptrcllem  38447  dfrcl2  38493  dfrcl3  38494  dftrcl3  38539  dfrtrcl3  38552  dfrtrcl4  38557  lhe4.4ex1a  39055  binomcxplemrat  39076  rnsnf  39891  feqresmptf  39952  limsupresre  40447  limsupvaluzmpt  40468  limsup10ex  40524  liminf10ex  40525  dvnprodlem1  40680  itgsin0pilem1  40684  wallispilem4  40803  wallispi2  40808  stirlinglem1  40809  stirlinglem3  40811  dirkercncflem2  40839  fourierdlem48  40889  fourierdlem49  40890  fourierdlem56  40897  fourierdlem57  40898  fourierdlem58  40899  fourierdlem62  40903  fourierdlem107  40948  fouriersw  40966  etransclem46  41015  sge0tsms  41115  sge0less  41127  sge0iun  41154  meadjun  41197  ovn02  41303  hoidmv1le  41329  hspmbllem2  41362  smflimsuplem3  41549
  Copyright terms: Public domain W3C validator