HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  wv Structured version   Unicode version

Definition wv 58
Description: The type of a typed variable.
Assertion
Ref Expression
wv |- x:al:al

Detailed syntax breakdown of Definition wv
StepHypRef Expression
1 hal . 2 type al
2 vx . . 3 var x
31, 2tv 1 . 2 term x:al
41, 3wffMMJ2t 12 1 wff x:al:al
Colors of variables: type var term
This definition is referenced by:  beta  82  insti  104  clf  105  cl  106  ovl  107  wal  124  wfal  125  wan  126  wim  127  wnot  128  wex  129  wor  130  weu  131  alval  132  exval  133  euval  134  notval  135  imval  136  orval  137  anval  138  ax4  140  pm2.21  143  dfan2  144  ecase  153  olc  154  orc  155  exlimdv2  156  exlimdv  157  ax4e  158  19.8a  160  eta  166  cbvf  167  cbv  168  leqf  169  exlimd  171  alimdv  172  eximdv  173  alnex  174  ac  184  dfex2  185  exmid  186  ax5  194  ax6  195  ax7  196  ax9  199  ax10  200  ax11  201  ax12  202  ax17  205  axext  206  axrep  207  axpow  208  axun  209
  Copyright terms: Public domain W3C validator