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

Theorem wal 124
Description: For all type.
Assertion
Ref Expression
wal |- A.:((al -> *) -> *)

Proof of Theorem wal
Dummy variables p x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wv 58 . . . 4 |- p:(al -> *):(al -> *)
2 wtru 40 . . . . 5 |- T.:*
32wl 59 . . . 4 |- \x:al T.:(al -> *)
41, 3weqi 68 . . 3 |- [p:(al -> *) = \x:al T.]:*
54wl 59 . 2 |- \p:(al -> *) [p:(al -> *) = \x:al T.]:((al -> *) -> *)
6 df-al 116 . 2 |- T. |= [A. = \p:(al -> *) [p:(al -> *) = \x:al T.]]
75, 6eqtypri 71 1 |- A.:((al -> *) -> *)
Colors of variables: type var term
Syntax hints:  tv 1   -> ht 2  *hb 3  \kl 6   = ke 7  T.kt 8  [kbr 9  wffMMJ2t 12  A.tal 112
This theorem is referenced by:  wfal  125  wex  129  wor  130  weu  131  alval  132  exval  133  euval  134  orval  137  ax4g  139  exlimdv2  156  ax4e  158  exlimd  171  alimdv  172  alnex  174  exnal1  175  ac  184  exnal  188  ax5  194  ax6  195  ax7  196  ax9  199  ax10  200  ax11  201  ax12  202  axext  206  axrep  207  axpow  208  axun  209
This theorem was proved from axioms:  ax-cb1 29  ax-refl 39
This theorem depends on definitions:  df-al 116
  Copyright terms: Public domain W3C validator