Theorem sbrimvwOLD 2104

Description: Obsolete version of sbrimvw 2103 as of 5-Jun-2026. (Contributed by Wolf Lammen, 29-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
sbrimvwOLD	⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem sbrimvwOLD

Step	Hyp	Ref	Expression
1		sb6 2097	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))
2		bi2.04 389	. . . 4 ⊢ ((𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝑥 = 𝑦 → (𝜑 → 𝜓)))
3	2	albii 1827	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))
4		19.21v 1947	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
5	1, 3, 4	3bitr2i 301	. 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
6		sb6 2097	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜓))
7	6	imbi2i 338	. 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
8	5, 7	bitr4i 280	1 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1546  [wsb 2074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075

This theorem is referenced by: (None)