Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  df-alsi GIF version

Definition df-alsi 10117
Description: Define "all some" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true and there is at least one 𝑥 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.)
Assertion
Ref Expression
df-alsi (∀!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑))

Detailed syntax breakdown of Definition df-alsi
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
3 vx . . 3 setvar 𝑥
41, 2, 3walsi 10115 . 2 wff ∀!𝑥(𝜑𝜓)
51, 2wi 4 . . . 4 wff (𝜑𝜓)
65, 3wal 1241 . . 3 wff 𝑥(𝜑𝜓)
71, 3wex 1381 . . 3 wff 𝑥𝜑
86, 7wa 97 . 2 wff (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑)
94, 8wb 98 1 wff (∀!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑))
Colors of variables: wff set class
This definition is referenced by:  alsconv  10119  alsi1d  10120  alsi2d  10121
  Copyright terms: Public domain W3C validator