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

Step	Hyp	Ref	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
8	5, 6, 7	kl 6	. . . . . 6 term λy:β A
9	3, 4, 8	kl 6	. . . . 5 term λx:α λy:β A
10		tb	. . . . 5 term B
11	9, 10	kc 5	. . . 4 term (λx:α λy:β AB)
12	2, 11	kc 5	. . 3 term ( = (λx:α λy:β AB))
13	3, 4, 7	kl 6	. . . . 5 term λx:α A
14	13, 10	kc 5	. . . 4 term (λx:α AB)
15	5, 6, 14	kl 6	. . 3 term λy:β (λx:α AB)
16	12, 15	kc 5	. 2 term (( = (λx:α λy:β AB))λy:β (λx:α AB))
17	1, 16	wffMMJ2 11	1 wff ⊤⊧(( = (λx:α λy:β AB))λy:β (λx:α AB))

This axiom is referenced by:  distrl  94