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

Metamath Proof Explorer

Theorem sbv

Description: Substitution for a variable not occurring in a proposition. See sbf for a version without disjoint variable condition on x , ph . If one adds a disjoint variable condition on x , t , then sbv can be proved directly by chaining equsv with sb6 . (Contributed by BJ, 22-Dec-2020)

		Ref	Expression
	Assertion	sbv	$⊢ [t/ x] φ \leftrightarrow φ$

Proof

Step	Hyp	Ref	Expression
1		spsbe	$⊢ [t/ x] φ \to \exists x φ$
2		ax5e	$⊢ \exists x φ \to φ$
3	1 2	syl	$⊢ [t/ x] φ \to φ$
4		ax-5	$⊢ φ \to \forall x φ$
5		stdpc4	$⊢ \forall x φ \to [t/ x] φ$
6	4 5	syl	$⊢ φ \to [t/ x] φ$
7	3 6	impbii	$⊢ [t/ x] φ \leftrightarrow φ$