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

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: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  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
  Copyright terms: Public domain W3C validator