Metamath Proof Explorer


Theorem equs5

Description: Lemma used in proofs of substitution properties. If there is a disjoint variable condition on x , y , then sbalex can be used instead; if y is not free in ph , then equs45f can be used. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 14-May-1993) (Revised by BJ, 1-Oct-2018) (New usage is discouraged.)

Ref Expression
Assertion equs5 ¬ x x = y x x = y φ x x = y φ

Proof

Step Hyp Ref Expression
1 nfna1 x ¬ x x = y
2 nfa1 x x x = y φ
3 axc15 ¬ x x = y x = y φ x x = y φ
4 3 impd ¬ x x = y x = y φ x x = y φ
5 1 2 4 exlimd ¬ x x = y x x = y φ x x = y φ
6 equs4 x x = y φ x x = y φ
7 5 6 impbid1 ¬ x x = y x x = y φ x x = y φ