Theorem sbv 2087

Description: Substitution for a variable not occurring in a proposition. See sbf 2270 for a version without disjoint variable condition on 𝑥, 𝜑. If one adds a disjoint variable condition on 𝑥, 𝑡, then sbv 2087 can be proved directly by chaining equsv 2001 with sb6 2084. (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 2081	. . 3 ⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑)
2		ax5e 1911	. . 3 ⊢ (∃𝑥𝜑 → 𝜑)
3	1, 2	syl 17	. 2 ⊢ ([𝑡 / 𝑥]𝜑 → 𝜑)
4		ax-5 1909	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
5		stdpc4 2067	. . 3 ⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
6	4, 5	syl 17	. 2 ⊢ (𝜑 → [𝑡 / 𝑥]𝜑)
7	3, 6	impbii 209	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 206  ∀wal 1537  ∃wex 1778  [wsb 2063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-sb 2064

This theorem is referenced by:  sbcom4  2088  sbievw  2092  sbievw2  2097  sbabel  2937  sbcg  3862  vn0  4344  eq0  4349  ab0w  4378  ab0orv  4382  eq0rdv  4406  rzal  4508  ralf0  4513  iuninc  32574  measiuns  34219  ballotlemodife  34501  xpab  35727  subsym1  36429  mptsnunlem  37340  ichv  47441  ichf  47442