Axiom ax-hbl1 103

Description: x is bound in λxA. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
ax-hbl1.1	⊢ A:γ
ax-hbl1.2	⊢ B:α

Assertion

Ref	Expression
ax-hbl1	⊢ ⊤⊧[(λx:α λx:β AB) = λx:β A]

Detailed syntax breakdown of Axiom ax-hbl1

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		hal	. . . . 5 type α
3		vx	. . . . 5 var x
4		hbe	. . . . . 6 type β
5		ta	. . . . . 6 term A
6	4, 3, 5	kl 6	. . . . 5 term λx:β A
7	2, 3, 6	kl 6	. . . 4 term λx:α λx:β A
8		tb	. . . 4 term B
9	7, 8	kc 5	. . 3 term (λx:α λx:β AB)
10		ke 7	. . 3 term =
11	9, 6, 10	kbr 9	. 2 term [(λx:α λx:β AB) = λx:β A]
12	1, 11	wffMMJ2 11	1 wff ⊤⊧[(λx:α λx:β AB) = λx:β A]

This axiom is referenced by:  hbl1  104  exlimdv  167  leqf  181  exlimd  183  alimdv  184  eximdv  185  alnex  186  exmid  199  ax5  207  ax6  208  ax7  209  ax9  212  axext  219  axrep  220