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	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		spsbe	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ∃ 𝑥 𝜑 )
2		ax5e	⊢ ( ∃ 𝑥 𝜑 → 𝜑 )
3	1 2	syl	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → 𝜑 )
4		ax-5	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
5		stdpc4	⊢ ( ∀ 𝑥 𝜑 → [ 𝑡 / 𝑥 ] 𝜑 )
6	4 5	syl	⊢ ( 𝜑 → [ 𝑡 / 𝑥 ] 𝜑 )
7	3 6	impbii	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ 𝜑 )