Definition df-alseu

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		wph	⊢ 𝜑
2		wps	⊢ 𝜓
3	1 2 0	walseu	⊢ ∀∃! 𝑥 ( 𝜑 → 𝜓 )
4	1 2	wi	⊢ ( 𝜑 → 𝜓 )
5	4 0	wal	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
6	1 0	weu	⊢ ∃! 𝑥 𝜑
7	5 6	wa	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 𝜑 )
8	3 7	wb	⊢ ( ∀∃! 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 𝜑 ) )