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	⊢ ⊤⊧[(λx:α By:α) = B]
ax-inst.3	⊢ ⊤⊧[(λx:α Sy:α) = S]
ax-inst.4	⊢ [x:α = C]⊧[A = B]
ax-inst.5	⊢ [x:α = 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