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 ] ph <-> ph )

Proof

Step	Hyp	Ref	Expression
1		spsbe	|- ( [ t / x ] ph -> E. x ph )
2		ax5e	|- ( E. x ph -> ph )
3	1 2	syl	|- ( [ t / x ] ph -> ph )
4		ax-5	|- ( ph -> A. x ph )
5		stdpc4	|- ( A. x ph -> [ t / x ] ph )
6	4 5	syl	|- ( ph -> [ t / x ] ph )
7	3 6	impbii	|- ( [ t / x ] ph <-> ph )