Definition df-rals 51313

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 51311	. 2 wff ∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓)
6	1, 2	wi 4	. . . 4 wff (𝜑 → 𝜓)
7	6, 3, 4	wral 3080	. . 3 wff ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
8	1, 3, 4	wrex 3090	. . 3 wff ∃𝑥 ∈ 𝐴 𝜑
9	7, 8	wa 401	. 2 wff (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑)
10	5, 9	wb 209	1 wff (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑))

This definition is used by:  dfrals2  51314  ralsd  51316  rals1d  51319  rals2d  51320  ralsex  51323  ralsbii  51325  nfrals  51328  ralrals  51332  rexrals  51333  ralsanmo  51335  ralseurals  51349