Definition df-ralseu 50600

Description: Define "all some one" applied to a class, which means 𝜓 is true whenever 𝜑 is true for 𝑥 in 𝐴, and exactly one 𝑥 in 𝐴 satisfies 𝜑. (Contributed by David A. Wheeler, 21-Jul-2026.)

Assertion

Ref	Expression
df-ralseu	⊢ (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))

Detailed syntax breakdown of Definition df-ralseu

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	wralseu 50598	. 2 wff ∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓)
6	1, 2	wi 4	. . . 4 wff (𝜑 → 𝜓)
7	6, 3, 4	wral 3079	. . 3 wff ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
8	1, 3, 4	wreu 3367	. . 3 wff ∃!𝑥 ∈ 𝐴 𝜑
9	7, 8	wa 400	. 2 wff (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑)
10	5, 9	wb 209	1 wff (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))

This definition is referenced by:  dfralseu2  50601  ralseurals  50603  ralseud  50605  ralseu1d  50608  ralseu2d  50609  ralseubii  50611  nfralseu  50613