Theorem wl-motae

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-motae	$$⊢{\exists }^{*}u\top \to \forall xy=z$$

Proof

Step	Hyp	Ref	Expression
1		wl-cbvmotv	$$⊢{\exists }^{*}u\top \to {\exists }^{*}v\top$$
2		wl-moteq	$$⊢{\exists }^{*}v\top \to y=z$$
3	2	alrimiv	$$⊢{\exists }^{*}v\top \to \forall xy=z$$
4	1 3	syl	$$⊢{\exists }^{*}u\top \to \forall xy=z$$