Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-17 GIF version

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
StepHypRef Expression
1 kt 8 . 2 term
2 hal . . . . 5 type α
3 vx . . . . 5 var x
4 ta . . . . 5 term A
52, 3, 4kl 6 . . . 4 term λx:α A
6 tb . . . 4 term B
75, 6kc 5 . . 3 term (λx:α AB)
8 ke 7 . . 3 term =
97, 4, 8kbr 9 . 2 term [(λx:α AB) = A]
101, 9wffMMJ2 11 1 wff ⊤⊧[(λx:α AB) = A]
 Colors of variables: type var term 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
 Copyright terms: Public domain W3C validator