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

Theorem mpteq2ia 5148
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 2819 . . 3 𝐴 = 𝐴
21ax-gen 1789 . 2 𝑥 𝐴 = 𝐴
3 mpteq2ia.1 . . 3 (𝑥𝐴𝐵 = 𝐶)
43rgen 3146 . 2 𝑥𝐴 𝐵 = 𝐶
5 mpteq12f 5140 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
62, 4, 5mp2an 690 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1528   = wceq 1530  wcel 2107  wral 3136  cmpt 5137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-ral 3141  df-opab 5120  df-mpt 5138
This theorem is referenced by:  mpteq2i  5149  feqresmpt  6727  elfvmptrab  6789  fmptap  6925  offres  7676  resixpfo  8492  dfoi  8967  cantnflem1d  9143  cantnflem1  9144  dfceil2  13201  dfid5  14378  dfid6  14379  cnrecnv  14516  ackbijnn  15175  harmonic  15206  ege2le3  15435  eirrlem  15549  prmrec  16250  imasdsval2  16781  smndex1iidm  18058  smndex2dlinvh  18074  cayleylem1  18532  pmtrprfval  18607  gsumzsplit  19039  gsum2dlem2  19083  dmdprdsplitlem  19151  coe1sclmul  20442  coe1sclmul2  20444  frlmip  20914  mdetunilem9  21221  leordtvallem1  21810  leordtvallem2  21811  txkgen  22252  cnmpt1st  22268  cnmpt2nd  22269  tmdgsum  22695  tsmssplit  22752  cnfldnm  23379  expcn  23472  pcorev2  23624  pi1xfrcnv  23653  rrxip  23985  mbfi1flim  24316  itg2uba  24336  itg2cnlem1  24354  itg2cnlem2  24355  itgitg2  24399  itgss3  24407  itgless  24409  ibladdlem  24412  itgaddlem1  24415  iblabslem  24420  itggt0  24434  itgcn  24435  limcdif  24466  limcres  24476  cnplimc  24477  dvcobr  24535  dvexp  24542  dveflem  24568  dvef  24569  dvlip  24582  dvlipcn  24583  lhop  24605  tdeglem2  24647  plyid  24791  coeidp  24845  dgrid  24846  pserdvlem2  25008  abelth  25021  dvrelog  25212  logcn  25222  dvlog  25226  advlog  25229  advlogexp  25230  logtayl  25235  logccv  25238  dvcxp1  25313  dvsqrt  25315  dvcncxp1  25316  dvcnsqrt  25317  resqrtcn  25322  loglesqrt  25331  logblog  25362  dvatan  25505  leibpilem2  25511  leibpi  25512  efrlim  25539  sqrtlim  25542  amgmlem  25559  emcllem5  25569  lgamgulmlem2  25599  lgam1  25633  chtublem  25779  logfacrlim2  25794  bposlem6  25857  chto1lb  26046  vmadivsum  26050  dchrvmasumlema  26068  mulogsumlem  26099  logdivsum  26101  logsqvma2  26111  log2sumbnd  26112  selberglem1  26113  selberglem3  26115  selberg  26116  selberg2lem  26118  selberg2  26119  pntrmax  26132  pntrsumo1  26133  selbergr  26136  selbergs  26142  pnt2  26181  pnt  26182  ostth2  26205  ostth  26207  hilnormi  28932  bra0  29719  partfun  30413  zrhre  31253  qqhre  31254  eulerpartgbij  31623  plymulx  31811  elmrsubrn  32760  faclim  32971  ptrest  34883  poimirlem19  34903  poimirlem20  34904  poimirlem30  34914  ovoliunnfl  34926  voliunnfl  34928  mbfposadd  34931  dvtan  34934  itg2addnclem  34935  ibladdnclem  34940  itgaddnclem1  34942  iblabsnclem  34947  itggt0cn  34956  ftc1anclem4  34962  ftc1anclem5  34963  ftc1anclem6  34964  ftc1anclem7  34965  ftc1anclem8  34966  dvasin  34970  dvacos  34971  areacirclem1  34974  arearect  39812  areaquad  39813  mptrcllem  39963  dfrcl2  40009  dfrcl3  40010  dftrcl3  40055  dfrtrcl3  40068  dfrtrcl4  40073  lhe4.4ex1a  40651  binomcxplemrat  40672  rnsnf  41433  feqresmptf  41488  limsupresre  41966  limsupvaluzmpt  41987  limsup10ex  42043  liminf10ex  42044  dvnprodlem1  42220  itgsin0pilem1  42224  wallispilem4  42343  wallispi2  42348  stirlinglem1  42349  stirlinglem3  42351  dirkercncflem2  42379  fourierdlem48  42429  fourierdlem49  42430  fourierdlem56  42437  fourierdlem57  42438  fourierdlem58  42439  fourierdlem62  42443  fourierdlem107  42488  fouriersw  42506  etransclem46  42555  sge0tsms  42652  sge0less  42664  sge0iun  42691  meadjun  42734  ovn02  42840  hoidmv1le  42866  hspmbllem2  42899  smflimsuplem3  43086
  Copyright terms: Public domain W3C validator