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 2262 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  2938  sbralie  3354  sbcg  3855  vn0  4337  eq0  4342  ab0w  4372  ab0OLD  4374  ab0orv  4377  eq0rdv  4403  rzal  4507  ralf0  4512  iuninc  31779  measiuns  33203  ballotlemodife  33484  xpab  34683  subsym1  35300  mptsnunlem  36207  ichv  46103  ichf  46104
  Copyright terms: Public domain W3C validator