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\top \to y=z$$

Proof

Step	Hyp	Ref	Expression
1		dfmo	$$⊢{\exists }^{*}x\top \leftrightarrow \exists w\forall x\left(\top \to x=w\right)$$
2		stdpc5v	$$⊢\forall x\left(\top \to x=w\right)\to \left(\top \to \forall xx=w\right)$$
3		tru	$$⊢\top$$
4	3	pm2.24i	$$⊢\neg \top \to y=z$$
5		aeveq	$$⊢\forall xx=w\to y=z$$
6	4 5	ja	$$⊢\left(\top \to \forall xx=w\right)\to y=z$$
7	2 6	syl	$$⊢\forall x\left(\top \to x=w\right)\to y=z$$
8	7	exlimiv	$$⊢\exists w\forall x\left(\top \to x=w\right)\to y=z$$
9	1 8	sylbi	$$⊢{\exists }^{*}x\top \to y=z$$