HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-distrl Structured version   Unicode version

Axiom ax-distrl 63
Description: Distribution of lambda abstraction over substitution.
Hypotheses
Ref Expression
ax-distrl.1 |- A:ga
ax-distrl.2 |- B:al
Assertion
Ref Expression
ax-distrl |- T. |= (( = (\x:al \y:be AB))\y:be (\x:al AB))
Distinct variable groups:   x,y   y,B

Detailed syntax breakdown of Axiom ax-distrl
StepHypRef Expression
1 kt 8 . 2 term T.
2 ke 7 . . . 4 term =
3 hal . . . . . 6 type al
4 vx . . . . . 6 var x
5 hbe . . . . . . 7 type be
6 vy . . . . . . 7 var y
7 ta . . . . . . 7 term A
85, 6, 7kl 6 . . . . . 6 term \y:be A
93, 4, 8kl 6 . . . . 5 term \x:al \y:be A
10 tb . . . . 5 term B
119, 10kc 5 . . . 4 term (\x:al \y:be AB)
122, 11kc 5 . . 3 term ( = (\x:al \y:be AB))
133, 4, 7kl 6 . . . . 5 term \x:al A
1413, 10kc 5 . . . 4 term (\x:al AB)
155, 6, 14kl 6 . . 3 term \y:be (\x:al AB)
1612, 15kc 5 . 2 term (( = (\x:al \y:be AB))\y:be (\x:al AB))
171, 16wffMMJ2 11 1 wff T. |= (( = (\x:al \y:be AB))\y:be (\x:al AB))
Colors of variables: type var term
This axiom is referenced by:  distrl  84
  Copyright terms: Public domain W3C validator