Theorem ralseurals

Description: "All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals . (Contributed by David A. Wheeler, 21-Jul-2026)

	Ref	Expression
Assertion	ralseurals	|- ( AE! x e. A ( ph -> ps ) -> AE x e. A ( ph -> ps ) )

Proof

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