Theorem bj-sbft

Description: Version of sbft using F// , proved from core axioms. (Contributed by BJ, 19-Nov-2023)

	Ref	Expression
Assertion	bj-sbft	$$⊢Ⅎ\text{'}x\phi \to \left(\left[t/x\right]\phi \leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spsbe	$$⊢\left[t/x\right]\phi \to \exists x\phi$$
2		bj-nnfe	$$⊢Ⅎ\text{'}x\phi \to \left(\exists x\phi \to \phi \right)$$
3	1 2	syl5	$$⊢Ⅎ\text{'}x\phi \to \left(\left[t/x\right]\phi \to \phi \right)$$
4		bj-nnfa	$$⊢Ⅎ\text{'}x\phi \to \left(\phi \to \forall x\phi \right)$$
5		stdpc4	$$⊢\forall x\phi \to \left[t/x\right]\phi$$
6	4 5	syl6	$$⊢Ⅎ\text{'}x\phi \to \left(\phi \to \left[t/x\right]\phi \right)$$
7	3 6	impbid	$$⊢Ⅎ\text{'}x\phi \to \left(\left[t/x\right]\phi \leftrightarrow \phi \right)$$