Theorem sbv 2089

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

Syntax hints:   ↔ wb 206  ∀wal 1538  ∃wex 1779  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-sb 2066

This theorem is referenced by:  sbcom4  2090  sbievw  2094  sbievw2  2099  sbabel  2925  sbcg  3829  vn0  4311  eq0  4316  ab0w  4345  ab0orv  4349  eq0rdv  4373  rzal  4475  ralf0  4480  iuninc  32496  measiuns  34214  ballotlemodife  34496  xpab  35720  subsym1  36422  mptsnunlem  37333  ichv  47454  ichf  47455