HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-17 Unicode 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:be
ax-17.2 |- B:al
Assertion
Ref Expression
ax-17 |- T. |= [(\x:al AB) = A]
Distinct variable group:   x,A

Detailed syntax breakdown of Axiom ax-17
StepHypRef Expression
1 kt 8 . 2 term T.
2 hal . . . . 5 type al
3 vx . . . . 5 var x
4 ta . . . . 5 term A
52, 3, 4kl 6 . . . 4 term \x:al A
6 tb . . . 4 term B
75, 6kc 5 . . 3 term (\x:al AB)
8 ke 7 . . 3 term =
97, 4, 8kbr 9 . 2 term [(\x:al AB) = A]
101, 9wffMMJ2 11 1 wff T. |= [(\x:al 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