Theorem alseuals

Description: "All some one" implies "all some": requiring exactly one witness is stronger than requiring at least one. Any consequence of an allsome statement is therefore a consequence of the corresponding "all some one" statement, which is how alseu-no-surprise is proved. (Contributed by David A. Wheeler, 21-Jul-2026)

	Ref	Expression
Assertion	alseuals	|- ( AE! x ( ph -> ps ) -> AE x ( ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		euex	|- ( E! x ph -> E. x ph )
2	1	anim2i	|- ( ( A. x ( ph -> ps ) /\ E! x ph ) -> ( A. x ( ph -> ps ) /\ E. x ph ) )
3		df-alseu	|- ( AE! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
4		df-als	|- ( AE x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
5	2 3 4	3imtr4i	|- ( AE! x ( ph -> ps ) -> AE x ( ph -> ps ) )