Theorem bj-sbft

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

	Ref	Expression
Assertion	bj-sbft	|- ( F// x ph -> ( [ t / x ] ph <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		spsbe	|- ( [ t / x ] ph -> E. x ph )
2		bj-nnfe	|- ( F// x ph -> ( E. x ph -> ph ) )
3	1 2	syl5	|- ( F// x ph -> ( [ t / x ] ph -> ph ) )
4		bj-nnfa	|- ( F// x ph -> ( ph -> A. x ph ) )
5		stdpc4	|- ( A. x ph -> [ t / x ] ph )
6	4 5	syl6	|- ( F// x ph -> ( ph -> [ t / x ] ph ) )
7	3 6	impbid	|- ( F// x ph -> ( [ t / x ] ph <-> ph ) )