Theorem bj-sbft

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

	Ref	Expression
Assertion	bj-sbft	⊢ ( Ⅎ' 𝑥 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜑 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		spsbe	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ∃ 𝑥 𝜑 )
2		bj-nnfe	⊢ ( Ⅎ' 𝑥 𝜑 → ( ∃ 𝑥 𝜑 → 𝜑 ) )
3	1 2	syl5	⊢ ( Ⅎ' 𝑥 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜑 → 𝜑 ) )
4		bj-nnfa	⊢ ( Ⅎ' 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) )
5		stdpc4	⊢ ( ∀ 𝑥 𝜑 → [ 𝑡 / 𝑥 ] 𝜑 )
6	4 5	syl6	⊢ ( Ⅎ' 𝑥 𝜑 → ( 𝜑 → [ 𝑡 / 𝑥 ] 𝜑 ) )
7	3 6	impbid	⊢ ( Ⅎ' 𝑥 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜑 ↔ 𝜑 ) )