Axiom ax-leq 69

Description: Equality theorem for abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
ax-leq.1	⊢ A:β
ax-leq.2	⊢ B:β
ax-leq.3	⊢ R⊧(( = A)B)

Assertion

Ref	Expression
ax-leq	⊢ R⊧(( = λx:α A)λx:α B)

Distinct variable group:   x,R

Detailed syntax breakdown of Axiom ax-leq

Step	Hyp	Ref	Expression
1		tr	. 2 term R
2		ke 7	. . . 4 term =
3		hal	. . . . 5 type α
4		vx	. . . . 5 var x
5		ta	. . . . 5 term A
6	3, 4, 5	kl 6	. . . 4 term λx:α A
7	2, 6	kc 5	. . 3 term ( = λx:α A)
8		tb	. . . 4 term B
9	3, 4, 8	kl 6	. . 3 term λx:α B
10	7, 9	kc 5	. 2 term (( = λx:α A)λx:α B)
11	1, 10	wffMMJ2 11	1 wff R⊧(( = λx:α A)λx:α B)

This axiom is referenced by:  leq  91