This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-sbft

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

		Ref	Expression
	Assertion	bj-sbft	$⊢ Ⅎ' x φ \to ([t/ x] φ \leftrightarrow φ)$

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