Theorem alsralrex

Description: The general "all some" quantifier with class membership as its antecedent holds if and only if ph holds for every x in A and some x in A satisfies ph . (Contributed by Peter Mazsa, 27-Nov-2018) (Revised by David A. Wheeler, 15-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		df-als	|- ( AE x ( x e. A -> ph ) <-> ( A. x ( x e. A -> ph ) /\ E. x x e. A ) )
2		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
3	2	bicomi	|- ( A. x ( x e. A -> ph ) <-> A. x e. A ph )
4	3	anbi1i	|- ( ( A. x ( x e. A -> ph ) /\ E. x x e. A ) <-> ( A. x e. A ph /\ E. x x e. A ) )
5		n0	|- ( A =/= (/) <-> E. x x e. A )
6	5	biimpri	|- ( E. x x e. A -> A =/= (/) )
7		r19.2z	|- ( ( A =/= (/) /\ A. x e. A ph ) -> E. x e. A ph )
8	6 7	sylan	|- ( ( E. x x e. A /\ A. x e. A ph ) -> E. x e. A ph )
9	8	expcom	|- ( A. x e. A ph -> ( E. x x e. A -> E. x e. A ph ) )
10		rexn0	|- ( E. x e. A ph -> A =/= (/) )
11	5	biimpi	|- ( A =/= (/) -> E. x x e. A )
12	10 11	syl	|- ( E. x e. A ph -> E. x x e. A )
13	12	a1i	|- ( A. x e. A ph -> ( E. x e. A ph -> E. x x e. A ) )
14	9 13	impbid	|- ( A. x e. A ph -> ( E. x x e. A <-> E. x e. A ph ) )
15	14	pm5.32i	|- ( ( A. x e. A ph /\ E. x x e. A ) <-> ( A. x e. A ph /\ E. x e. A ph ) )
16	4 15	bitri	|- ( ( A. x ( x e. A -> ph ) /\ E. x x e. A ) <-> ( A. x e. A ph /\ E. x e. A ph ) )
17	1 16	bitri	|- ( AE x ( x e. A -> ph ) <-> ( A. x e. A ph /\ E. x e. A ph ) )