Theorem exexw

Description: Existential quantification is idempotent. Weak version of bj-exexbiex , requiring fewer axioms. (Contributed by Gino Giotto, 4-Nov-2024)

	Ref	Expression
Hypothesis	exexw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	exexw	⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		exexw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2	1	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3	2	hba1w	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 )
4	2	spw	⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ 𝜑 )
5	4	alimi	⊢ ( ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 )
6	3 5	impbii	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 )
7	6	notbii	⊢ ( ¬ ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 )
8		df-ex	⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )
9		2exnaln	⊢ ( ∃ 𝑥 ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 )
10	7 8 9	3bitr4i	⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑥 𝜑 )