Axiom ax-17 105

Description: If x does not appear in A, then any substitution to A yields A again, i.e. λxA is a constant function. (Contributed by Mario Carneiro, 8-Oct-2014.)

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  106  insti  114  cl  116  exlimdv  167  cbvf  179  cbv  180  leqf  181  exlimd  183  alimdv  184  eximdv  185  alnex  186  exmid  199  ax5  207  ax6  208  ax7  209  ax9  212  ax12  215  ax17m  218  axext  219  axrep  220