Definition df-fal 127

Description: Define the constant false. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

Ref	Expression
df-fal	|- T. |= [F. = (A.\p:* p:*)]

Detailed syntax breakdown of Definition df-fal

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		tfal 118	. . 3 term F.
3		tal 122	. . . 4 term A.
4		hb 3	. . . . 5 type *
5		vp	. . . . 5 var p
6	4, 5	tv 1	. . . . 5 term p:*
7	4, 5, 6	kl 6	. . . 4 term \p:* p:*
8	3, 7	kc 5	. . 3 term (A.\p:* p:*)
9		ke 7	. . 3 term =
10	2, 8, 9	kbr 9	. 2 term [F. = (A.\p:* p:*)]
11	1, 10	wffMMJ2 11	1 wff T. |= [F. = (A.\p:* p:*)]

This definition is referenced by:  wfal  135  pm2.21  153