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	|- ( ( AE x ( ph -> ps ) /\ E* x ph ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-als	|- ( AE x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
2	1	anbi1i	|- ( ( AE x ( ph -> ps ) /\ E* x ph ) <-> ( ( A. x ( ph -> ps ) /\ E. x ph ) /\ E* x ph ) )
3		anass	|- ( ( ( A. x ( ph -> ps ) /\ E. x ph ) /\ E* x ph ) <-> ( A. x ( ph -> ps ) /\ ( E. x ph /\ E* x ph ) ) )
4		df-eu	|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
5	4	bicomi	|- ( ( E. x ph /\ E* x ph ) <-> E! x ph )
6	5	anbi2i	|- ( ( A. x ( ph -> ps ) /\ ( E. x ph /\ E* x ph ) ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
7	2 3 6	3bitri	|- ( ( AE x ( ph -> ps ) /\ E* x ph ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )