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

Theorem sbrimvw 2100
 Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2310 and sbrimv 2311 based on fewer axioms, but with more disjoint variable conditions. Based on an idea of Gino Giotto. (Contributed by Wolf Lammen, 29-Jan-2024.)
Assertion
Ref Expression
sbrimvw ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem sbrimvw
StepHypRef Expression
1 19.21v 1941 . 2 (∀𝑥(𝜑 → (𝑥 = 𝑦𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦𝜓)))
21sbrimvlem 2099 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  [wsb 2070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071 This theorem is referenced by:  sbiedvw  2102
 Copyright terms: Public domain W3C validator