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 Gino Giotto, 20-Nov-2024)

Ref Expression
Hypothesis sbrim.1 ⊢Ⅎxφ
Assertion sbrim ⊢yxφ→ψ↔φ→yxψ

Proof

Step Hyp Ref Expression
1 sbrim.1 ⊢Ⅎxφ
2 bi2.04 ⊢x=t→φ→ψ↔φ→x=t→ψ
3 2 albii ⊢∀xx=t→φ→ψ↔∀xφ→x=t→ψ
4 1 19.21 ⊢∀xφ→x=t→ψ↔φ→∀xx=t→ψ
5 3 4 bitri ⊢∀xx=t→φ→ψ↔φ→∀xx=t→ψ
6 5 imbi2i ⊢t=y→∀xx=t→φ→ψ↔t=y→φ→∀xx=t→ψ
7 bi2.04 ⊢t=y→φ→∀xx=t→ψ↔φ→t=y→∀xx=t→ψ
8 6 7 bitri ⊢t=y→∀xx=t→φ→ψ↔φ→t=y→∀xx=t→ψ
9 8 albii ⊢∀tt=y→∀xx=t→φ→ψ↔∀tφ→t=y→∀xx=t→ψ
10 df-sb ⊢yxφ→ψ↔∀tt=y→∀xx=t→φ→ψ
11 df-sb ⊢yxψ↔∀tt=y→∀xx=t→ψ
12 11 imbi2i ⊢φ→yxψ↔φ→∀tt=y→∀xx=t→ψ
13 19.21v ⊢∀tφ→t=y→∀xx=t→ψ↔φ→∀tt=y→∀xx=t→ψ
14 12 13 bitr4i ⊢φ→yxψ↔∀tφ→t=y→∀xx=t→ψ
15 9 10 14 3bitr4i ⊢yxφ→ψ↔φ→yxψ