Metamath Proof Explorer

Theorem bj-sbievw2

Description: Lemma for substitution. (Contributed by BJ, 23-Jul-2023)

Ref Expression
Assertion bj-sbievw2 ⊢ y x ψ → φ → ψ → y x φ

Proof

Step Hyp Ref Expression
1 sb6 ⊢ y x ψ → φ ↔ ∀ x x = y → ψ → φ
2 bj-sblem2 ⊢ ∀ x x = y → ψ → φ → ∃ x x = y → ψ → ∀ x x = y → φ
3 jarr ⊢ ∃ x x = y → ψ → ∀ x x = y → φ → ψ → ∀ x x = y → φ
4 sb6 ⊢ y x φ ↔ ∀ x x = y → φ
5 3 4 imbitrrdi ⊢ ∃ x x = y → ψ → ∀ x x = y → φ → ψ → y x φ
6 2 5 syl ⊢ ∀ x x = y → ψ → φ → ψ → y x φ
7 1 6 sylbi ⊢ y x ψ → φ → ψ → y x φ