Definition df-rals 50624

Description: Define "all some" applied to a class, which means 𝜓 is true whenever 𝜑 is true for 𝑥 in 𝐴, and there is at least one 𝑥 in 𝐴 where 𝜑 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 is, that the formula held throughout 𝐴 and that 𝐴 had at least one member. I've now decided that that was a mistake. Its older existence conjunct ∃𝑥𝑥 ∈ 𝐴 did not require any member of 𝐴 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	⊢ (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑))

Detailed syntax breakdown of Definition df-rals

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		vx	. . 3 setvar 𝑥
4		cA	. . 3 class 𝐴
5	1, 2, 3, 4	wrals 50622	. 2 wff ∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓)
6	1, 2	wi 4	. . . 4 wff (𝜑 → 𝜓)
7	6, 3, 4	wral 3081	. . 3 wff ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
8	1, 3, 4	wrex 3091	. . 3 wff ∃𝑥 ∈ 𝐴 𝜑
9	7, 8	wa 401	. 2 wff (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑)
10	5, 9	wb 209	1 wff (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑))

This definition is used by:  dfrals2  50625  ralsd  50627  rals1d  50630  rals2d  50631  ralsex  50634  ralsbii  50636  nfrals  50639  ralrals  50643  rexrals  50644  ralsanmo  50646  ralseurals  50660