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

Syntax Definition walsi 12824
Description: Extend wff definition to include "all some" applied to a top-level implication, which means  ps is true whenever 
ph is true, and there is at least least one  x where  ph is true. (Contributed by David A. Wheeler, 20-Oct-2018.)
Ref Expression
wph  wff  ph
wps  wff  ps
vx  setvar  x
Ref Expression
walsi  wff  A.! x
( ph  ->  ps )

See definition df-alsi 12826 for more information.

Colors of variables: wff set class
  Copyright terms: Public domain W3C validator