Definition df-ralseu 17137

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, 22-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 17135	. 2 wff ∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓)
6	1, 2	wi 4	. . . 4 wff (𝜑 → 𝜓)
7	6, 3, 4	wral 2528	. . 3 wff ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
8	1, 3, 4	wreu 2530	. . 3 wff ∃!𝑥 ∈ 𝐴 𝜑
9	7, 8	wa 104	. 2 wff (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑)
10	5, 9	wb 105	1 wff (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))

This definition is referenced by:  dfralseu2  17138  ralseurals  17140  ralseud  17142  ralseu1d  17145  ralseu2d  17146  ralseubii  17148  nfralseu  17150