Metamath Proof Explorer


Theorem wl-moteq

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of KalishMontague p. 86. (Contributed by Wolf Lammen, 5-Mar-2023)

Ref Expression
Assertion wl-moteq *xy=z

Proof

Step Hyp Ref Expression
1 df-mo *xwxx=w
2 stdpc5v xx=wxx=w
3 tru
4 3 pm2.24i ¬y=z
5 aeveq xx=wy=z
6 4 5 ja xx=wy=z
7 2 6 syl xx=wy=z
8 7 exlimiv wxx=wy=z
9 1 8 sylbi *xy=z