Theorem rexrals

Description: If a member of A satisfying the antecedent exists, then a restricted "all some" statement reduces to its universal part. This is the restricted counterpart of rexals . (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026)

	Ref	Expression
Assertion	rexrals	|- ( E. x e. A ph -> ( AE x e. A ( ph -> ps ) <-> A. x e. A ( ph -> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-rals	|- ( AE x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )
2		iba	|- ( E. x e. A ph -> ( A. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) ) )
3	2	bicomd	|- ( E. x e. A ph -> ( ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) <-> A. x e. A ( ph -> ps ) ) )
4	1 3	bitrid	|- ( E. x e. A ph -> ( AE x e. A ( ph -> ps ) <-> A. x e. A ( ph -> ps ) ) )