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

Definition df-alsi 11056
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.)
Assertion
Ref Expression
df-alsi  |-  ( A.! x ( ph  ->  ps )  <->  ( A. x
( ph  ->  ps )  /\  E. x ph )
)

Detailed syntax breakdown of Definition df-alsi
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
3 vx . . 3  setvar  x
41, 2, 3walsi 11054 . 2  wff  A.! x
( ph  ->  ps )
51, 2wi 4 . . . 4  wff  ( ph  ->  ps )
65, 3wal 1283 . . 3  wff  A. x
( ph  ->  ps )
71, 3wex 1422 . . 3  wff  E. x ph
86, 7wa 102 . 2  wff  ( A. x ( ph  ->  ps )  /\  E. x ph )
94, 8wb 103 1  wff  ( A.! x ( ph  ->  ps )  <->  ( A. x
( ph  ->  ps )  /\  E. x ph )
)
Colors of variables: wff set class
This definition is referenced by:  alsconv  11058  alsi1d  11059  alsi2d  11060
  Copyright terms: Public domain W3C validator