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

Metamath Proof Explorer

Theorem sbievw

Description: Conversion of implicit substitution to explicit substitution. Version of sbie and sbiev with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994) (Revised by BJ, 18-Jul-2023) (Proof shortened by SN, 24-Aug-2025)

Ref Expression
Hypothesis sbievw.is ⊢ x = y → φ ↔ ψ
Assertion sbievw ⊢ y x φ ↔ ψ

Proof

Step Hyp Ref Expression
1 sbievw.is ⊢ x = y → φ ↔ ψ
2 1 sbbiiev ⊢ y x φ ↔ y x ψ
3 sbv ⊢ y x ψ ↔ ψ
4 2 3 bitri ⊢ y x φ ↔ ψ