Theorem wv 64

Description: The type of a typed variable. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

Ref	Expression
wv	⊢ x:α:α

Proof of Theorem wv

Step	Hyp	Ref	Expression
1		ax-wv 63	1 ⊢ x:α:α

Syntax hints:  tv 1  wffMMJ2t 12

This theorem was proved from axioms:  ax-wv 63

This theorem is referenced by:  beta  92  insti  114  clf  115  cl  116  ovl  117  wal  134  wfal  135  wan  136  wim  137  wnot  138  wex  139  wor  140  weu  141  alval  142  exval  143  euval  144  notval  145  imval  146  orval  147  anval  148  ax4  150  pm2.21  153  dfan2  154  ecase  163  olc  164  orc  165  exlimdv2  166  exlimdv  167  ax4e  168  19.8a  170  eta  178  cbvf  179  cbv  180  leqf  181  exlimd  183  alimdv  184  eximdv  185  alnex  186  ac  197  dfex2  198  exmid  199  ax5  207  ax6  208  ax7  209  ax9  212  ax10  213  ax11  214  ax12  215  ax17m  218  axext  219  axrep  220  axpow  221  axun  222