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 1539  ∃wex 1781  [wsb 2067

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

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

This theorem is referenced by:  sbcom4  2092  sbievw2  2099  sbabel  2939  sbcg  3816  vn0  4296  eq0  4301  ab0w  4331  ab0OLD  4333  ab0orv  4336  eq0rdv  4362  rzal  4464  ralf0  4469  iuninc  31308  measiuns  32628  ballotlemodife  32909  xpab  34109  subsym1  34837  mptsnunlem  35747  ichv  45542  ichf  45543