Theorem sbv 2088

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

Syntax hints:   ↔ wb 206  ∀wal 1535  ∃wex 1777  [wsb 2064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-sb 2065

This theorem is referenced by:  sbcom4  2089  sbievw  2093  sbievw2  2098  sbabel  2944  sbcg  3883  vn0  4368  eq0  4373  ab0w  4401  ab0OLD  4403  ab0orv  4406  eq0rdv  4430  rzal  4532  ralf0  4537  iuninc  32583  measiuns  34181  ballotlemodife  34462  xpab  35688  subsym1  36393  mptsnunlem  37304  ichv  47323  ichf  47324