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: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

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

This axiom is referenced by:  distrl  94