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

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

Proof of Theorem sbrimvw
StepHypRef Expression
1 sb6 2083 . . 3 ([𝑦 / 𝑥](𝜑𝜓) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑𝜓)))
2 bi2.04 387 . . . 4 ((𝜑 → (𝑥 = 𝑦𝜓)) ↔ (𝑥 = 𝑦 → (𝜑𝜓)))
32albii 1816 . . 3 (∀𝑥(𝜑 → (𝑥 = 𝑦𝜓)) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑𝜓)))
4 19.21v 1937 . . 3 (∀𝑥(𝜑 → (𝑥 = 𝑦𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦𝜓)))
51, 3, 43bitr2i 299 . 2 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦𝜓)))
6 sb6 2083 . . 3 ([𝑦 / 𝑥]𝜓 ↔ ∀𝑥(𝑥 = 𝑦𝜓))
76imbi2i 336 . 2 ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦𝜓)))
85, 7bitr4i 278 1 ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535  [wsb 2062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063
This theorem is referenced by:  sbiedvw  2093  cbvralsvw  3315
  Copyright terms: Public domain W3C validator