Definition df-rals 17129

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 ph to the members of a class, asserting only ( A. x e. A ph /\ E. x x e. A ), that is, 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 E. x x e. A 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.)

Assertion

Ref	Expression
df-rals	|- ( A.E. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )

Detailed syntax breakdown of Definition df-rals

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		vx	. . 3 setvar x
4		cA	. . 3 class A
5	1, 2, 3, 4	wrals 17127	. 2 wff A.E. x e. A ( ph -> ps )
6	1, 2	wi 4	. . . 4 wff ( ph -> ps )
7	6, 3, 4	wral 2528	. . 3 wff A. x e. A ( ph -> ps )
8	1, 3, 4	wrex 2529	. . 3 wff E. x e. A ph
9	7, 8	wa 104	. 2 wff ( A. x e. A ( ph -> ps ) /\ E. x e. A ph )
10	5, 9	wb 105	1 wff ( A.E. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )

This definition is used by:  dfrals2  17130  ralsd  17132  rals1d  17135  rals2d  17136  ralsex  17140  ralsbii  17142  nfrals  17145  ralrals  17149  rexrals  17150  ralsanmo  17152  ralseurals  17166