Axiom ax-hbl1 103

Description: x is bound in \xA. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
ax-hbl1.1	|- A:ga
ax-hbl1.2	|- B:al

Assertion

Ref	Expression
ax-hbl1	|- T. |= [(\x:al \x:be AB) = \x:be A]

Detailed syntax breakdown of Axiom ax-hbl1

Step	Hyp	Ref	Expression
1		kt 8	. 2 term T.
2		hal	. . . . 5 type al
3		vx	. . . . 5 var x
4		hbe	. . . . . 6 type be
5		ta	. . . . . 6 term A
6	4, 3, 5	kl 6	. . . . 5 term \x:be A
7	2, 3, 6	kl 6	. . . 4 term \x:al \x:be A
8		tb	. . . 4 term B
9	7, 8	kc 5	. . 3 term (\x:al \x:be AB)
10		ke 7	. . 3 term =
11	9, 6, 10	kbr 9	. 2 term [(\x:al \x:be AB) = \x:be A]
12	1, 11	wffMMJ2 11	1 wff T. |= [(\x:al \x:be AB) = \x:be A]

This axiom is referenced by:  hbl1  104  exlimdv  167  leqf  181  exlimd  183  alimdv  184  eximdv  185  alnex  186  exmid  199  ax5  207  ax6  208  ax7  209  ax9  212  axext  219  axrep  220