Metamath Proof Explorer

Theorem bj-sbievw

Description: Lemma for substitution. Closed form of equsalvw and sbievw . (Contributed by BJ, 23-Jul-2023)

Ref Expression
Assertion bj-sbievw ⊢ y x φ ↔ ψ → y x φ ↔ ψ

Proof

Step Hyp Ref Expression
1 sb6 ⊢ y x φ ↔ ψ ↔ ∀ x x = y → φ ↔ ψ
2 bj-sblem ⊢ ∀ 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 3bitr4g ⊢ ∀ x x = y → φ ↔ ψ → y x φ ↔ ψ
7 1 6 sylbi ⊢ y x φ ↔ ψ → y x φ ↔ ψ