This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbrimvwOLD

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

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

Proof

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