Metamath Proof Explorer


Theorem bj-equs45fv

Description: Version of equs45f with a disjoint variable condition, which does not require ax-13 . Note that the version of equs5 with a disjoint variable condition is actually sbalex (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis bj-equs45fv.1 y φ
Assertion bj-equs45fv x x = y φ x x = y φ

Proof

Step Hyp Ref Expression
1 bj-equs45fv.1 y φ
2 1 nf5ri φ y φ
3 2 anim2i x = y φ x = y y φ
4 3 eximi x x = y φ x x = y y φ
5 equs5av x x = y y φ x x = y φ
6 4 5 syl x x = y φ x x = y φ
7 equs4v x x = y φ x x = y φ
8 6 7 impbii x x = y φ x x = y φ