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

Theorem mpteq2ia 4518
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 2505 . . 3 𝐴 = 𝐴
21ax-gen 1698 . 2 𝑥 𝐴 = 𝐴
3 mpteq2ia.1 . . 3 (𝑥𝐴𝐵 = 𝐶)
43rgen 2801 . 2 𝑥𝐴 𝐵 = 𝐶
5 mpteq12f 4511 . 2 ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥𝐴 𝐵 = 𝐶) → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
62, 4, 5mp2an 695 1 (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1466   = wceq 1468  wcel 1937  wral 2791  cmpt 4493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-ral 2796  df-opab 4494  df-mpt 4495
This theorem is referenced by:  mpteq2i  4519  feqresmpt  5984  elfvmptrab  6038  fmptap  6155  offres  6865  resixpfo  7643  dfoi  8109  cantnflem1d  8278  cantnflem1  8279  dfceil2  12176  dfid5  13250  dfid6  13251  cnrecnv  13388  ackbijnn  14046  harmonic  14077  ege2le3  14304  eirrlem  14416  prmrec  15028  imasdsval2  15582  imasdsval2OLD  15594  cayleylem1  17214  pmtrprfval  17289  gsumzsplit  17721  gsum2dlem2  17764  dmdprdsplitlem  17830  coe1sclmul  19034  coe1sclmul2  19036  frlmip  19494  mdetunilem9  19803  leordtvallem1  20383  leordtvallem2  20384  txkgen  20824  cnmpt1st  20840  cnmpt2nd  20841  tmdgsum  21268  tsmssplit  21324  cnfldnm  21957  expcn  22062  pcorev2  22218  pi1xfrcnv  22247  rrxip  22508  mbfi1flim  22842  itg2uba  22862  itg2cnlem1  22880  itg2cnlem2  22881  itgitg2  22925  itgss3  22933  itgless  22935  ibladdlem  22938  itgaddlem1  22941  iblabslem  22946  itggt0  22960  itgcn  22961  limcdif  22992  limcres  23002  cnplimc  23003  dvcobr  23061  dvexp  23068  dveflem  23092  dvef  23093  dvlip  23106  dvlipcn  23107  lhop  23129  tdeglem2  23171  plyid  23324  coeidp  23378  dgrid  23379  pserdvlem2  23544  abelth  23557  dvrelog  23743  logcn  23753  dvlog  23757  advlog  23760  advlogexp  23761  logtayl  23766  logccv  23769  dvcxp1  23841  dvsqrt  23843  dvcncxp1  23844  dvcnsqrt  23845  resqrtcn  23850  loglesqrt  23859  logblog  23890  dvatan  24022  leibpilem2  24028  leibpi  24029  efrlim  24056  sqrtlim  24059  amgmlem  24076  emcllem5  24086  lgamgulmlem2  24116  lgam1  24150  chtublem  24300  logfacrlim2  24315  bposlem6  24378  chto1lb  24477  vmadivsum  24481  dchrvmasumlema  24499  mulogsumlem  24530  logdivsum  24532  logsqvma2  24542  log2sumbnd  24543  selberglem1  24544  selberglem3  24546  selberg  24547  selberg2lem  24549  selberg2  24550  pntrmax  24563  pntrsumo1  24564  selbergr  24567  selbergs  24573  pnt2  24612  pnt  24613  ostth2  24636  ostth  24638  hilnormi  26979  bra0  27766  partfun  28435  zrhre  28978  qqhre  28979  eulerpartgbij  29359  plymulx  29590  faclim  30533  ptrest  32177  poimirlem19  32197  poimirlem20  32198  poimirlem30  32208  ovoliunnfl  32220  voliunnfl  32222  mbfposadd  32226  dvtan  32230  itg2addnclem  32231  ibladdnclem  32236  itgaddnclem1  32238  iblabsnclem  32243  itggt0cn  32252  ftc1anclem4  32258  ftc1anclem5  32259  ftc1anclem6  32260  ftc1anclem7  32261  ftc1anclem8  32262  dvasin  32266  dvacos  32267  areacirclem1  32270  arearect  36340  areaquad  36341  mptrcllem  36459  dfrcl2  36505  dfrcl3  36506  dftrcl3  36551  dfrtrcl3  36564  dfrtrcl4  36569  lhe4.4ex1a  37035  binomcxplemrat  37056  rnsnf  37818  dvnprodlem1  38240  itgsin0pilem1  38245  wallispilem4  38366  wallispi2  38371  stirlinglem1  38372  stirlinglem3  38374  dirkercncflem2  38402  fourierdlem48  38454  fourierdlem49  38455  fourierdlem56  38462  fourierdlem57  38463  fourierdlem58  38464  fourierdlem62  38468  fourierdlem107  38513  fouriersw  38531  etransclem46  38581  sge0tsms  38668  sge0less  38680  sge0iun  38707  meadjun  38750  ovn02  38853  hoidmv1le  38879  hspmbllem2  38912
  Copyright terms: Public domain W3C validator