Definition df-ralseu

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		wph	⊢ 𝜑
3		wps	⊢ 𝜓
4	2 3 0 1	wralseu	⊢ ∀∃! 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 )
5	2 3	wi	⊢ ( 𝜑 → 𝜓 )
6	5 0 1	wral	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 )
7	2 0 1	wreu	⊢ ∃! 𝑥 ∈ 𝐴 𝜑
8	6 7	wa	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 ∈ 𝐴 𝜑 )
9	4 8	wb	⊢ ( ∀∃! 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) )