MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpt2eq3ia Unicode version

Theorem mpt2eq3ia 6362
Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Hypothesis
Ref Expression
mpt2eq3ia.1
Assertion
Ref Expression
mpt2eq3ia

Proof of Theorem mpt2eq3ia
StepHypRef Expression
1 mpt2eq3ia.1 . . . 4
213adant1 1014 . . 3
32mpt2eq3dva 6361 . 2
43trud 1404 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395   wtru 1396  e.wcel 1818  e.cmpt2 6298
This theorem is referenced by:  mpt2difsnif  6395  mpt2snif  6396  oprab2co  6885  cnfcomlem  8164  cnfcom2  8167  cnfcomlemOLD  8172  cnfcom2OLD  8175  dfioo2  11654  elovmpt2wrd  12583  sadcom  14113  comfffval2  15096  oppchomf  15115  symgga  16431  oppglsm  16662  dfrhm2  17366  cnfldsub  18446  cnflddiv  18448  mat0op  18921  mattpos1  18958  mdetunilem7  19120  madufval  19139  maducoeval2  19142  madugsum  19145  mp2pm2mplem5  19311  mp2pm2mp  19312  leordtval  19714  xpstopnlem1  20310  divcn  21372  oprpiece1res1  21451  oprpiece1res2  21452  cxpcn  23119  wwlknprop  24686  numclwwlk5  25112  numclwwlk7  25114  cnnvm  25588  cnre2csqima  27893  mndpluscn  27908  raddcn  27911  mendplusgfval  31134  dflinc2  33011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-oprab 6300  df-mpt2 6301
  Copyright terms: Public domain W3C validator