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 φ ψ