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.

Step	Hyp	Ref	Expression
1		wv 64	. . . 4 ⊢ p:(α → ∗):(α → ∗)
2		wtru 43	. . . . 5 ⊢ ⊤:∗
3	2	wl 66	. . . 4 ⊢ λx:α ⊤:(α → ∗)
4	1, 3	weqi 76	. . 3 ⊢ [p:(α → ∗) = λx:α ⊤]:∗
5	4	wl 66	. 2 ⊢ λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]:((α → ∗) → ∗)
6		df-al 126	. 2 ⊢ ⊤⊧[∀ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]
7	5, 6	eqtypri 81	1 ⊢ ∀:((α → ∗) → ∗)

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