Definition df-alsi

Description: Define "all some" applied to a top-level implication, which means ps is true whenever ph is true and there is at least one x where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018)

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

Detailed syntax breakdown

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