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

Step	Hyp	Ref	Expression
1		ts	. 2 term S
2		tb	. 2 term B
3	1, 2	wffMMJ2 11	1 wff S |= B

This axiom is referenced by:  insti  114  leqf  181  ax9  212