Definition df-al 126

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

Assertion

Ref	Expression
df-al	|- T. |= [A. = \p:(al -> *) [p:(al -> *) = \x:al T.]]

Distinct variable group:   x,p

Detailed syntax breakdown of Definition df-al

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		tal 122	. . 3 term A.
3		hal	. . . . 5 type al
4		hb 3	. . . . 5 type *
5	3, 4	ht 2	. . . 4 type (al -> *)
6		vp	. . . 4 var p
7	5, 6	tv 1	. . . . 5 term p:(al -> *)
8		vx	. . . . . 6 var x
9	3, 8, 1	kl 6	. . . . 5 term \x:al T.
10		ke 7	. . . . 5 term =
11	7, 9, 10	kbr 9	. . . 4 term [p:(al -> *) = \x:al T.]
12	5, 6, 11	kl 6	. . 3 term \p:(al -> *) [p:(al -> *) = \x:al T.]
13	2, 12, 10	kbr 9	. 2 term [A. = \p:(al -> *) [p:(al -> *) = \x:al T.]]
14	1, 13	wffMMJ2 11	1 wff T. |= [A. = \p:(al -> *) [p:(al -> *) = \x:al T.]]

This definition is referenced by:  wal  134  alval  142