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

Theorem sbv 2091
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 2091 can be proved directly by chaining equsv 2006 with sb6 2088. (Contributed by BJ, 22-Dec-2020.)
Assertion
Ref Expression
sbv ([𝑡 / 𝑥]𝜑𝜑)
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜑(𝑡)

Proof of Theorem sbv
StepHypRef Expression
1 spsbe 2085 . . 3 ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑)
2 ax5e 1915 . . 3 (∃𝑥𝜑𝜑)
31, 2syl 17 . 2 ([𝑡 / 𝑥]𝜑𝜑)
4 ax-5 1913 . . 3 (𝜑 → ∀𝑥𝜑)
5 stdpc4 2071 . . 3 (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
64, 5syl 17 . 2 (𝜑 → [𝑡 / 𝑥]𝜑)
73, 6impbii 208 1 ([𝑡 / 𝑥]𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wal 1539  wex 1781  [wsb 2067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971
This theorem depends on definitions:  df-bi 206  df-ex 1782  df-sb 2068
This theorem is referenced by:  sbcom4  2092  sbievw2  2099  sbabel  2939  sbcg  3816  vn0  4296  eq0  4301  ab0w  4331  ab0OLD  4333  ab0orv  4336  eq0rdv  4362  rzal  4464  ralf0  4469  iuninc  31308  measiuns  32628  ballotlemodife  32909  xpab  34109  subsym1  34837  mptsnunlem  35747  ichv  45542  ichf  45543
  Copyright terms: Public domain W3C validator