Definition df-al 126

Description: Define the for all operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

Ref	Expression
df-al	⊢ ⊤⊧[∀ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]

Distinct variable group:   x,p

Detailed syntax breakdown of Definition df-al

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tal 122	. . 3 term ∀
3		hal	. . . . 5 type α
4		hb 3	. . . . 5 type ∗
5	3, 4	ht 2	. . . 4 type (α → ∗)
6		vp	. . . 4 var p
7	5, 6	tv 1	. . . . 5 term p:(α → ∗)
8		vx	. . . . . 6 var x
9	3, 8, 1	kl 6	. . . . 5 term λx:α ⊤
10		ke 7	. . . . 5 term =
11	7, 9, 10	kbr 9	. . . 4 term [p:(α → ∗) = λx:α ⊤]
12	5, 6, 11	kl 6	. . 3 term λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]
13	2, 12, 10	kbr 9	. 2 term [∀ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]
14	1, 13	wffMMJ2 11	1 wff ⊤⊧[∀ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]

This definition is referenced by:  wal  134  alval  142