Theorem ralrals

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

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

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		ibar	|- ( A. x e. A ( ph -> ps ) -> ( E. x e. A ph <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) ) )
3	2	bicomd	|- ( A. x e. A ( ph -> ps ) -> ( ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) <-> E. x e. A ph ) )
4	1 3	bitrid	|- ( A. x e. A ( ph -> ps ) -> ( AE x e. A ( ph -> ps ) <-> E. x e. A ph ) )