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  2924  sbcg  3826  vn0  4308  eq0  4313  ab0w  4342  ab0orv  4346  eq0rdv  4370  rzal  4472  ralf0  4477  iuninc  32489  measiuns  34207  ballotlemodife  34489  xpab  35713  subsym1  36415  mptsnunlem  37326  ichv  47450  ichf  47451