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

Metamath Proof Explorer

Theorem sbrim

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 4-Oct-2016) Avoid ax-10 . (Revised by GG, 20-Nov-2024)

Ref Expression
Hypothesis sbrim.1 ⊢ Ⅎ 𝑥 𝜑
Assertion sbrim ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )

Proof

Step Hyp Ref Expression
1 sbrim.1 ⊢ Ⅎ 𝑥 𝜑
2 bi2.04 ⊢ ( ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ↔ ( 𝜑 → ( 𝑥 = 𝑡 → 𝜓 ) ) )
3 2 albii ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ↔ ∀ 𝑥 ( 𝜑 → ( 𝑥 = 𝑡 → 𝜓 ) ) )
4 1 19.21 ⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝑥 = 𝑡 → 𝜓 ) ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) )
5 3 4 bitri ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) )
6 5 imbi2i ⊢ ( ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ) ↔ ( 𝑡 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
7 bi2.04 ⊢ ( ( 𝑡 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) ↔ ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
8 6 7 bitri ⊢ ( ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ) ↔ ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
9 8 albii ⊢ ( ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ) ↔ ∀ 𝑡 ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
10 dfsb ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → ( 𝜑 → 𝜓 ) ) ) )
11 dfsb ⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) )
12 11 imbi2i ⊢ ( ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( 𝜑 → ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
13 19.21v ⊢ ( ∀ 𝑡 ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
14 12 13 bitr4i ⊢ ( ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ∀ 𝑡 ( 𝜑 → ( 𝑡 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) ) )
15 9 10 14 3bitr4i ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )