Theorem sbv 2091

Description: Substitution for a variable not occurring in a proposition. See sbf 2262 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  2938  sbralie  3354  sbcg  3855  vn0  4337  eq0  4342  ab0w  4372  ab0OLD  4374  ab0orv  4377  eq0rdv  4403  rzal  4507  ralf0  4512  iuninc  31779  measiuns  33203  ballotlemodife  33484  xpab  34683  subsym1  35300  mptsnunlem  36207  ichv  46103  ichf  46104