Definition df-rals 51068

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

This definition is used by:  dfrals2  51069  ralsd  51071  rals1d  51074  rals2d  51075  ralsex  51078  ralsbii  51080  nfrals  51083  ralrals  51087  rexrals  51088  ralsanmo  51090  ralseurals  51104