Theorem wal 124

Description: For all type.

Assertion

Ref	Expression
wal	⊢ ∀:((α → ∗) → ∗)

Proof of Theorem wal

Dummy variables p x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wv 58	. . . 4 ⊢ p:(α → ∗):(α → ∗)
2		wtru 40	. . . . 5 ⊢ ⊤:∗
3	2	wl 59	. . . 4 ⊢ λx:α ⊤:(α → ∗)
4	1, 3	weqi 68	. . 3 ⊢ [p:(α → ∗) = λx:α ⊤]:∗
5	4	wl 59	. 2 ⊢ λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]:((α → ∗) → ∗)
6		df-al 116	. 2 ⊢ ⊤⊧[∀ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]
7	5, 6	eqtypri 71	1 ⊢ ∀:((α → ∗) → ∗)

Syntax hints:  tv 1   → ht 2  ∗hb 3  λkl 6   = ke 7  ⊤kt 8  [kbr 9  wffMMJ2t 12  ∀tal 112

This theorem was proved from axioms:  ax-cb1 29  ax-refl 39

This theorem depends on definitions:  df-al 116

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