Metamath Proof Explorer


Theorem bj-eqs

Description: A lemma for substitutions, proved from Tarski's FOL. The version without DV ( x , y ) is true but requires ax-13 . The disjoint variable condition DV ( x , ph ) is necessary for both directions: consider substituting x = z for ph . (Contributed by BJ, 25-May-2021)

Ref Expression
Assertion bj-eqs φ x x = y φ

Proof

Step Hyp Ref Expression
1 ax-1 φ x = y φ
2 1 alrimiv φ x x = y φ
3 exim x x = y φ x x = y x φ
4 ax6ev x x = y
5 pm2.27 x x = y x x = y x φ x φ
6 4 5 ax-mp x x = y x φ x φ
7 ax5e x φ φ
8 3 6 7 3syl x x = y φ φ
9 2 8 impbii φ x x = y φ