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

Theorem wal 134
Description: For all type. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
wal :((α → ∗) → ∗)

Proof of Theorem wal
Dummy variables p x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wv 64 . . . 4 p:(α → ∗):(α → ∗)
2 wtru 43 . . . . 5 ⊤:∗
32wl 66 . . . 4 λx:α ⊤:(α → ∗)
41, 3weqi 76 . . 3 [p:(α → ∗) = λx:α ⊤]:∗
54wl 66 . 2 λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]:((α → ∗) → ∗)
6 df-al 126 . 2 ⊤⊧[ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]
75, 6eqtypri 81 1 :((α → ∗) → ∗)
Colors of variables: type var term
Syntax hints:  tv 1  ht 2  hb 3  λkl 6   = ke 7  kt 8  [kbr 9  wffMMJ2t 12  tal 122
This theorem was proved from axioms:  ax-cb1 29  ax-weq 40  ax-refl 42  ax-wv 63  ax-wl 65  ax-wov 71  ax-eqtypri 80
This theorem depends on definitions:  df-al 126
This theorem is referenced by:  wfal  135  wex  139  wor  140  weu  141  alval  142  exval  143  euval  144  orval  147  ax4g  149  exlimdv2  166  ax4e  168  exlimd  183  alimdv  184  alnex  186  exnal1  187  ac  197  exnal  201  ax5  207  ax6  208  ax7  209  ax9  212  ax10  213  ax11  214  ax12  215  axext  219  axrep  220  axpow  221  axun  222
  Copyright terms: Public domain W3C validator