Theorem bj-moeub

Description: Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022)

	Ref	Expression
Assertion	bj-moeub	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ↔ ∃! 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		moeu	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
2		euex	⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑥 𝜑 )
3		impbi	⊢ ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) → ( ( ∃! 𝑥 𝜑 → ∃ 𝑥 𝜑 ) → ( ∃ 𝑥 𝜑 ↔ ∃! 𝑥 𝜑 ) ) )
4	2 3	mpi	⊢ ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) → ( ∃ 𝑥 𝜑 ↔ ∃! 𝑥 𝜑 ) )
5		biimp	⊢ ( ( ∃ 𝑥 𝜑 ↔ ∃! 𝑥 𝜑 ) → ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
6	4 5	impbii	⊢ ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜑 ↔ ∃! 𝑥 𝜑 ) )
7	1 6	bitri	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ↔ ∃! 𝑥 𝜑 ) )