Metamath Proof Explorer

Theorem bj-sbievw1

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

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

Proof

Step Hyp Ref Expression
1 sb6 ⊢ y x φ → ψ ↔ ∀ x x = y → φ → ψ
2 bj-sblem1 ⊢ ∀ x x = y → φ → ψ → ∀ x x = y → φ → ∃ x x = y → ψ
3 sb6 ⊢ y x φ ↔ ∀ x x = y → φ
4 ax6ev ⊢ ∃ x x = y
5 4 a1bi ⊢ ψ ↔ ∃ x x = y → ψ
6 2 3 5 3imtr4g ⊢ ∀ x x = y → φ → ψ → y x φ → ψ
7 1 6 sylbi ⊢ y x φ → ψ → y x φ → ψ