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

Theorem mpteq2ia 4731
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 2620 . . 3 𝐴 = 𝐴
21ax-gen 1720 . 2 𝑥 𝐴 = 𝐴
3 mpteq2ia.1 . . 3 (𝑥𝐴𝐵 = 𝐶)
43rgen 2919 . 2 𝑥𝐴 𝐵 = 𝐶
5 mpteq12f 4722 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
62, 4, 5mp2an 707 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479   = wceq 1481  wcel 1988  wral 2909  cmpt 4720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-ral 2914  df-opab 4704  df-mpt 4721
This theorem is referenced by:  mpteq2i  4732  feqresmpt  6237  elfvmptrab  6292  fmptap  6421  offres  7148  resixpfo  7931  dfoi  8401  cantnflem1d  8570  cantnflem1  8571  dfceil2  12623  dfid5  13748  dfid6  13749  cnrecnv  13886  ackbijnn  14541  harmonic  14572  ege2le3  14801  eirrlem  14913  prmrec  15607  imasdsval2  16157  cayleylem1  17813  pmtrprfval  17888  gsumzsplit  18308  gsum2dlem2  18351  dmdprdsplitlem  18417  coe1sclmul  19633  coe1sclmul2  19635  frlmip  20098  mdetunilem9  20407  leordtvallem1  20995  leordtvallem2  20996  txkgen  21436  cnmpt1st  21452  cnmpt2nd  21453  tmdgsum  21880  tsmssplit  21936  cnfldnm  22563  expcn  22656  pcorev2  22809  pi1xfrcnv  22838  rrxip  23159  mbfi1flim  23471  itg2uba  23491  itg2cnlem1  23509  itg2cnlem2  23510  itgitg2  23554  itgss3  23562  itgless  23564  ibladdlem  23567  itgaddlem1  23570  iblabslem  23575  itggt0  23589  itgcn  23590  limcdif  23621  limcres  23631  cnplimc  23632  dvcobr  23690  dvexp  23697  dveflem  23723  dvef  23724  dvlip  23737  dvlipcn  23738  lhop  23760  tdeglem2  23802  plyid  23946  coeidp  24000  dgrid  24001  pserdvlem2  24163  abelth  24176  dvrelog  24364  logcn  24374  dvlog  24378  advlog  24381  advlogexp  24382  logtayl  24387  logccv  24390  dvcxp1  24462  dvsqrt  24464  dvcncxp1  24465  dvcnsqrt  24466  resqrtcn  24471  loglesqrt  24480  logblog  24511  dvatan  24643  leibpilem2  24649  leibpi  24650  efrlim  24677  sqrtlim  24680  amgmlem  24697  emcllem5  24707  lgamgulmlem2  24737  lgam1  24771  chtublem  24917  logfacrlim2  24932  bposlem6  24995  chto1lb  25148  vmadivsum  25152  dchrvmasumlema  25170  mulogsumlem  25201  logdivsum  25203  logsqvma2  25213  log2sumbnd  25214  selberglem1  25215  selberglem3  25217  selberg  25218  selberg2lem  25220  selberg2  25221  pntrmax  25234  pntrsumo1  25235  selbergr  25238  selbergs  25244  pnt2  25283  pnt  25284  ostth2  25307  ostth  25309  hilnormi  27990  bra0  28779  partfun  29449  zrhre  30037  qqhre  30038  eulerpartgbij  30408  plymulx  30599  faclim  31607  ptrest  33379  poimirlem19  33399  poimirlem20  33400  poimirlem30  33410  ovoliunnfl  33422  voliunnfl  33424  mbfposadd  33428  dvtan  33431  itg2addnclem  33432  ibladdnclem  33437  itgaddnclem1  33439  iblabsnclem  33444  itggt0cn  33453  ftc1anclem4  33459  ftc1anclem5  33460  ftc1anclem6  33461  ftc1anclem7  33462  ftc1anclem8  33463  dvasin  33467  dvacos  33468  areacirclem1  33471  arearect  37620  areaquad  37621  mptrcllem  37739  dfrcl2  37785  dfrcl3  37786  dftrcl3  37831  dfrtrcl3  37844  dfrtrcl4  37849  lhe4.4ex1a  38348  binomcxplemrat  38369  rnsnf  39186  feqresmptf  39249  limsupresre  39728  limsupvaluzmpt  39749  limsup10ex  39799  liminf10ex  39800  dvnprodlem1  39924  itgsin0pilem1  39928  wallispilem4  40048  wallispi2  40053  stirlinglem1  40054  stirlinglem3  40056  dirkercncflem2  40084  fourierdlem48  40134  fourierdlem49  40135  fourierdlem56  40142  fourierdlem57  40143  fourierdlem58  40144  fourierdlem62  40148  fourierdlem107  40193  fouriersw  40211  etransclem46  40260  sge0tsms  40360  sge0less  40372  sge0iun  40399  meadjun  40442  ovn02  40545  hoidmv1le  40571  hspmbllem2  40604  smflimsuplem3  40791
  Copyright terms: Public domain W3C validator