Axiom ax-beta 67

Description: Axiom of beta-substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypothesis

Ref	Expression
ax-beta.1	⊢ A:β

Assertion

Ref	Expression
ax-beta	⊢ ⊤⊧(( = (λx:α Ax:α))A)

Detailed syntax breakdown of Axiom ax-beta

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

This axiom is referenced by:  beta  92