HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-hbl1 Unicode 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:ga
ax-hbl1.2 |- B:al
Assertion
Ref Expression
ax-hbl1 |- T. |= [(\x:al \x:be AB) = \x:be A]

Detailed syntax breakdown of Axiom ax-hbl1
StepHypRef Expression
1 kt 8 . 2 term T.
2 hal . . . . 5 type al
3 vx . . . . 5 var x
4 hbe . . . . . 6 type be
5 ta . . . . . 6 term A
64, 3, 5kl 6 . . . . 5 term \x:be A
72, 3, 6kl 6 . . . 4 term \x:al \x:be A
8 tb . . . 4 term B
97, 8kc 5 . . 3 term (\x:al \x:be AB)
10 ke 7 . . 3 term =
119, 6, 10kbr 9 . 2 term [(\x:al \x:be AB) = \x:be A]
121, 11wffMMJ2 11 1 wff T. |= [(\x:al \x:be AB) = \x:be 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