MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbv Structured version   Visualization version   GIF version

Theorem sbv 2087
Description: Substitution for a variable not occurring in a proposition. See sbf 2270 for a version without disjoint variable condition on 𝑥, 𝜑. If one adds a disjoint variable condition on 𝑥, 𝑡, then sbv 2087 can be proved directly by chaining equsv 2001 with sb6 2084. (Contributed by BJ, 22-Dec-2020.)
Assertion
Ref Expression
sbv ([𝑡 / 𝑥]𝜑𝜑)
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜑(𝑡)

Proof of Theorem sbv
StepHypRef Expression
1 spsbe 2081 . . 3 ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑)
2 ax5e 1911 . . 3 (∃𝑥𝜑𝜑)
31, 2syl 17 . 2 ([𝑡 / 𝑥]𝜑𝜑)
4 ax-5 1909 . . 3 (𝜑 → ∀𝑥𝜑)
5 stdpc4 2067 . . 3 (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
64, 5syl 17 . 2 (𝜑 → [𝑡 / 𝑥]𝜑)
73, 6impbii 209 1 ([𝑡 / 𝑥]𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wal 1537  wex 1778  [wsb 2063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966
This theorem depends on definitions:  df-bi 207  df-ex 1779  df-sb 2064
This theorem is referenced by:  sbcom4  2088  sbievw  2092  sbievw2  2097  sbabel  2937  sbcg  3862  vn0  4344  eq0  4349  ab0w  4378  ab0orv  4382  eq0rdv  4406  rzal  4508  ralf0  4513  iuninc  32574  measiuns  34219  ballotlemodife  34501  xpab  35727  subsym1  36429  mptsnunlem  37340  ichv  47441  ichf  47442
  Copyright terms: Public domain W3C validator