Metamath Proof Explorer


Theorem equsexv

Description: An equivalence related to implicit substitution. Version of equsex with a disjoint variable condition, which does not require ax-13 . See equsexvw for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv . (Contributed by NM, 5-Aug-1993) (Revised by BJ, 31-May-2019) Avoid ax-10 . (Revised by GG, 18-Nov-2024)

Ref Expression
Hypotheses equsalv.nf xψ
equsalv.1 x=yφψ
Assertion equsexv xx=yφψ

Proof

Step Hyp Ref Expression
1 equsalv.nf xψ
2 equsalv.1 x=yφψ
3 2 biimpa x=yφψ
4 1 3 exlimi xx=yφψ
5 1 2 equsalv xx=yφψ
6 equs4v xx=yφxx=yφ
7 5 6 sylbir ψxx=yφ
8 4 7 impbii xx=yφψ