Definition df-fal 127

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

Assertion

Ref	Expression
df-fal	⊢ ⊤⊧[⊥ = (∀λp:∗ p:∗)]

Detailed syntax breakdown of Definition df-fal

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tfal 118	. . 3 term ⊥
3		tal 122	. . . 4 term ∀
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 (∀λp:∗ p:∗)
9		ke 7	. . 3 term =
10	2, 8, 9	kbr 9	. 2 term [⊥ = (∀λp:∗ p:∗)]
11	1, 10	wffMMJ2 11	1 wff ⊤⊧[⊥ = (∀λp:∗ p:∗)]

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