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)

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


Step Hyp Ref Expression
1 x ψ
2 equsalv.1 x = y φ ψ
3 2 pm5.32i x = y φ x = y ψ
4 3 exbii x x = y φ x x = y ψ
5 ax6ev x x = y
6 1 19.41 x x = y ψ x x = y ψ
7 5 6 mpbiran x x = y ψ ψ
8 4 7 bitri x x = y φ ψ