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

Axiom ax-inst 113
Description: Instantiate a theorem with a new term. The second and third hypotheses are the HOL equivalent of set.mm "effectively not free in" predicate (see set.mm's ax-17, or ax17m 218). (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
ax-inst.1 |- R |= A
ax-inst.2 |- T. |= [(\x:al By:al) = B]
ax-inst.3 |- T. |= [(\x:al Sy:al) = S]
ax-inst.4 |- [x:al = C] |= [A = B]
ax-inst.5 |- [x:al = C] |= [R = S]
Assertion
Ref Expression
ax-inst |- S |= B
Distinct variable groups:   x,y   y,B   y,S

Detailed syntax breakdown of Axiom ax-inst
StepHypRef Expression
1 ts . 2 term S
2 tb . 2 term B
31, 2wffMMJ2 11 1 wff S |= B
Colors of variables: type var term
This axiom is referenced by:  insti  114  leqf  181  ax9  212
  Copyright terms: Public domain W3C validator