# 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 ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\top \to {y}={z}$

### Proof

Step Hyp Ref Expression
1 df-mo ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\top ↔\exists {w}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\top \to {x}={w}\right)$
2 stdpc5v ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\top \to {x}={w}\right)\to \left(\top \to \forall {x}\phantom{\rule{.4em}{0ex}}{x}={w}\right)$
3 tru ${⊢}\top$
4 3 pm2.24i ${⊢}¬\top \to {y}={z}$
5 aeveq ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={w}\to {y}={z}$
6 4 5 ja ${⊢}\left(\top \to \forall {x}\phantom{\rule{.4em}{0ex}}{x}={w}\right)\to {y}={z}$
7 2 6 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\top \to {x}={w}\right)\to {y}={z}$
8 7 exlimiv ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\top \to {x}={w}\right)\to {y}={z}$
9 1 8 sylbi ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\top \to {y}={z}$