Axiom ax-beta 67

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

Hypothesis

Ref	Expression
ax-beta.1	|- A:be

Assertion

Ref	Expression
ax-beta	|- T. |= (( = (\x:al Ax:al))A)

Detailed syntax breakdown of Axiom ax-beta

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		ta	. . . . . 6 term A
6	3, 4, 5	kl 6	. . . . 5 term \x:al A
7	3, 4	tv 1	. . . . 5 term x:al
8	6, 7	kc 5	. . . 4 term (\x:al Ax:al)
9	2, 8	kc 5	. . 3 term ( = (\x:al Ax:al))
10	9, 5	kc 5	. 2 term (( = (\x:al Ax:al))A)
11	1, 10	wffMMJ2 11	1 wff T. |= (( = (\x:al Ax:al))A)

This axiom is referenced by:  beta  92