Theorem sbv 2091

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

Assertion

Ref	Expression
sbv	⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑)

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜑(𝑡)

Proof of Theorem sbv

Step	Hyp	Ref	Expression
1		spsbe 2085	. . 3 ⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑)
2		ax5e 1915	. . 3 ⊢ (∃𝑥𝜑 → 𝜑)
3	1, 2	syl 17	. 2 ⊢ ([𝑡 / 𝑥]𝜑 → 𝜑)
4		ax-5 1913	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
5		stdpc4 2071	. . 3 ⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
6	4, 5	syl 17	. 2 ⊢ (𝜑 → [𝑡 / 𝑥]𝜑)
7	3, 6	impbii 208	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 205  ∀wal 1537  ∃wex 1782  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-sb 2068

This theorem is referenced by:  sbcom4  2092  sbievw2  2099  sbabel  2941  sbcg  3795  vn0  4272  eq0  4277  ab0w  4307  ab0OLD  4309  ab0orv  4312  eq0rdv  4338  rzal  4439  ralf0  4444  iuninc  30900  measiuns  32185  ballotlemodife  32464  xpab  33677  mptsnunlem  35509  ichv  44901  ichf  44902