Axiom ax-17 95

Description: If x does not appear in A, then any substitution to A yields A again, i.e. λxA is a constant function.

Hypotheses

Ref	Expression
ax-17.1	⊢ A:β
ax-17.2	⊢ B:α

Assertion

Ref	Expression
ax-17	⊢ ⊤⊧[(λx:α AB) = A]

Distinct variable group:   x,A

Detailed syntax breakdown of Axiom ax-17

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

This axiom is referenced by:  a17i  96  insti  104  cl  106  exlimdv  157  cbvf  167  cbv  168  leqf  169  exlimd  171  alimdv  172  eximdv  173  alnex  174  exmid  186  ax5  194  ax6  195  ax7  196  ax9  199  ax12  202  ax17  205  axext  206  axrep  207