Definition df-rals

Description: Define "all some" applied to a class, which means ps is true whenever ph is true for x in A , and there is at least one x in A where ph is true.

An older definition of the "all some" quantifier when scoped to a class, named df-alsc and now removed, instead applied a bare formula to the members of a class, asserting only that the formula held throughout A and that A had at least one member. I've now decided that that was a mistake. Its older existence conjunct did not require any member of A to satisfy the antecedent, so if the formula was itself an implication, that inner implication could still be vacuously true, which is precisely what the allsome quantifier exists to prevent. For example, the older definition meant that "among Martians, all tall ones are green" could be considered true if there are Martians, but no tall Martians. This version of the definition instead ensures that claims of the form "among Martians, all tall ones are green" can only be true if all tall Martians are green and that there is at least one tall Martian. (Contributed by David A. Wheeler, 20-Oct-2018) (Revised by David A. Wheeler, 12-Jul-2026)

	Ref	Expression
Assertion	df-rals	Could not format assertion : No typesetting found for |- ( AE x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3		wps	$$wff\psi$$
4	2 3 0 1	wrals	Could not format AE x e. A ( ph -> ps ) : No typesetting found for wff AE x e. A ( ph -> ps ) with typecode wff
5	2 3	wi	$$wff\left(\phi \to \psi \right)$$
6	5 0 1	wral	$$wff\forall x\in A\left(\phi \to \psi \right)$$
7	2 0 1	wrex	$$wff\exists x\in A\phi$$
8	6 7	wa	$$wff\left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists x\in A\phi \right)$$
9	4 8	wb	Could not format ( AE x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) ) : No typesetting found for wff ( AE x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) ) with typecode wff