Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-hbl1 GIF version

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
StepHypRef Expression
1 kt 8 . 2 term
2 hal . . . . 5 type α
3 vx . . . . 5 var x
4 hbe . . . . . 6 type β
5 ta . . . . . 6 term A
64, 3, 5kl 6 . . . . 5 term λx:β A
72, 3, 6kl 6 . . . 4 term λx:α λx:β A
8 tb . . . 4 term B
97, 8kc 5 . . 3 term (λx:α λx:β AB)
10 ke 7 . . 3 term =
119, 6, 10kbr 9 . 2 term [(λx:α λx:β AB) = λx:β A]
121, 11wffMMJ2 11 1 wff ⊤⊧[(λx:α λx:β AB) = λx:β A]
 Colors of variables: type var term 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
 Copyright terms: Public domain W3C validator