Theorem sbv 2086

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

Syntax hints:   ↔ wb 206  ∀wal 1535  ∃wex 1776  [wsb 2062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-sb 2063

This theorem is referenced by:  sbcom4  2087  sbievw  2091  sbievw2  2096  sbabel  2936  sbcg  3870  vn0  4351  eq0  4356  ab0w  4385  ab0orv  4389  eq0rdv  4413  rzal  4515  ralf0  4520  iuninc  32581  measiuns  34198  ballotlemodife  34479  xpab  35706  subsym1  36410  mptsnunlem  37321  ichv  47374  ichf  47375