Theorem wl-cbvmotv

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-cbvmotv	$$⊢{\exists }^{*}x\top \to {\exists }^{*}y\top$$

Proof

Step	Hyp	Ref	Expression
1		ax7v2	$$⊢x=y\to \left(x=z\to y=z\right)$$
2	1	imim2d	$$⊢x=y\to \left(\left(\top \to x=z\right)\to \left(\top \to y=z\right)\right)$$
3	2	cbvalivw	$$⊢\forall x\left(\top \to x=z\right)\to \forall y\left(\top \to y=z\right)$$
4	3	eximi	$$⊢\exists z\forall x\left(\top \to x=z\right)\to \exists z\forall y\left(\top \to y=z\right)$$
5		dfmo	$$⊢{\exists }^{*}x\top \leftrightarrow \exists z\forall x\left(\top \to x=z\right)$$
6		dfmo	$$⊢{\exists }^{*}y\top \leftrightarrow \exists z\forall y\left(\top \to y=z\right)$$
7	4 5 6	3imtr4i	$$⊢{\exists }^{*}x\top \to {\exists }^{*}y\top$$