Theorem rexals

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

	Ref	Expression
Assertion	rexals	|- ( E. x e. A ph -> ( AE x ( x e. A -> ph ) <-> A. 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		iba	|- ( E. x e. A ph -> ( A. x e. A ph <-> ( A. x e. A ph /\ E. x e. A ph ) ) )
3	2	bicomd	|- ( E. x e. A ph -> ( ( A. x e. A ph /\ E. x e. A ph ) <-> A. x e. A ph ) )
4	1 3	bitrid	|- ( E. x e. A ph -> ( AE x ( x e. A -> ph ) <-> A. x e. A ph ) )