Theorem sbv 2092

Description: Substitution for a variable not occurring in a proposition. See sbf 2266 for a version without disjoint variable condition on 𝑥, 𝜑. If one adds a disjoint variable condition on 𝑥, 𝑡, then sbv 2092 can be proved directly by chaining equsv 2007 with sb6 2089. (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 2086	. . 3 ⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑)
2		ax5e 1916	. . 3 ⊢ (∃𝑥𝜑 → 𝜑)
3	1, 2	syl 17	. 2 ⊢ ([𝑡 / 𝑥]𝜑 → 𝜑)
4		ax-5 1914	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
5		stdpc4 2072	. . 3 ⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
6	4, 5	syl 17	. 2 ⊢ (𝜑 → [𝑡 / 𝑥]𝜑)
7	3, 6	impbii 208	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 205  ∀wal 1537  ∃wex 1783  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-sb 2069

This theorem is referenced by:  sbcom4  2093  sbievw2  2101  sbabel  2940  sbcg  3791  vn0  4269  eq0  4274  ab0w  4304  ab0OLD  4306  ab0orv  4309  eq0rdv  4335  rzal  4436  ralf0  4441  iuninc  30801  measiuns  32085  ballotlemodife  32364  xpab  33579  mptsnunlem  35436  ichv  44789  ichf  44790