Theorem alsanmo

Description: An "all some" statement conjoined with the claim that at most one x satisfies its antecedent is equivalent to the universal part conjoined with the claim that exactly one x satisfies the antecedent. The "all some" quantifier supplies the existence of such an x and E* x ph supplies the at-most-one part, so together they yield E! x ph . (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026)

	Ref	Expression
Assertion	alsanmo	⊢ ( ( ∀∃ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃* 𝑥 𝜑 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-als	⊢ ( ∀∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 𝜑 ) )
2	1	anbi1i	⊢ ( ( ∀∃ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃* 𝑥 𝜑 ) ↔ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 𝜑 ) ∧ ∃* 𝑥 𝜑 ) )
3		anass	⊢ ( ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 𝜑 ) ∧ ∃* 𝑥 𝜑 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ) )
4		df-eu	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )
5	4	bicomi	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ↔ ∃! 𝑥 𝜑 )
6	5	anbi2i	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 𝜑 ) )
7	2 3 6	3bitri	⊢ ( ( ∀∃ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃* 𝑥 𝜑 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 𝜑 ) )