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

Syntax Definition walsc 12825
Description: Extend wff definition to include "all some" applied to a class, which means  ph is true for all  x in  A, and there is at least one  x in  A. (Contributed by David A. Wheeler, 20-Oct-2018.)
Ref Expression
wph  wff  ph
vx  setvar  x
cA  class  A
Ref Expression
walsc  wff  A.! x  e.  A ph

See definition df-alsc 12827 for more information.

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