Theorem sbv 2092

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 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 1540  ∃wex 1782  [wsb 2068

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

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

This theorem is referenced by:  sbcom4  2093  sbievw2  2100  sbabel  2939  sbralie  3355  sbcg  3857  vn0  4339  eq0  4344  ab0w  4374  ab0OLD  4376  ab0orv  4379  eq0rdv  4405  rzal  4509  ralf0  4514  iuninc  31792  measiuns  33215  ballotlemodife  33496  xpab  34695  subsym1  35312  mptsnunlem  36219  ichv  46117  ichf  46118