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	⊢ ( ∃* 𝑥 ⊤ → 𝑦 = 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		dfmo	⊢ ( ∃* 𝑥 ⊤ ↔ ∃ 𝑤 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑤 ) )
2		stdpc5v	⊢ ( ∀ 𝑥 ( ⊤ → 𝑥 = 𝑤 ) → ( ⊤ → ∀ 𝑥 𝑥 = 𝑤 ) )
3		tru	⊢ ⊤
4	3	pm2.24i	⊢ ( ¬ ⊤ → 𝑦 = 𝑧 )
5		aeveq	⊢ ( ∀ 𝑥 𝑥 = 𝑤 → 𝑦 = 𝑧 )
6	4 5	ja	⊢ ( ( ⊤ → ∀ 𝑥 𝑥 = 𝑤 ) → 𝑦 = 𝑧 )
7	2 6	syl	⊢ ( ∀ 𝑥 ( ⊤ → 𝑥 = 𝑤 ) → 𝑦 = 𝑧 )
8	7	exlimiv	⊢ ( ∃ 𝑤 ∀ 𝑥 ( ⊤ → 𝑥 = 𝑤 ) → 𝑦 = 𝑧 )
9	1 8	sylbi	⊢ ( ∃* 𝑥 ⊤ → 𝑦 = 𝑧 )