Theorem ralals

Description: If ph holds for every x in A , then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that some x in A satisfies ph . See ralrals for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018) (Revised by David A. Wheeler, 15-Jul-2026)

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

Proof

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