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

Axiom ax-distrl 70
 Description: Distribution of lambda abstraction over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
ax-distrl.1 A:γ
ax-distrl.2 B:α
Assertion
Ref Expression
ax-distrl ⊤⊧(( = (λx:α λy:β AB))λy:β (λx:α AB))
Distinct variable groups:   x,y   y,B

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