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

Definition df-alsi 46192
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 46190 . 2 wff ∀!𝑥(𝜑𝜓)
51, 2wi 4 . . . 4 wff (𝜑𝜓)
65, 3wal 1541 . . 3 wff 𝑥(𝜑𝜓)
71, 3wex 1787 . . 3 wff 𝑥𝜑
86, 7wa 399 . 2 wff (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑)
94, 8wb 209 1 wff (∀!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  alsconv  46194  alsi1d  46195  alsi2d  46196  alsi-no-surprise  46200
  Copyright terms: Public domain W3C validator