NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  wal Structured version   Unicode version

Syntax Definition wal 1540
Description: Extend wff definition to include the universal quantifier ('for all'). is read " (phi) is true for all ." Typically, in its final application would be replaced with a wff containing a (free) occurrence of the variable , for example . In a universe with a finite number of objects, "for all" is equivalent to a big conjunction (AND) with one wff for each possible case of . When the universe is infinite (as with set theory), such a propositional-calculus equivalent is not possible because an infinitely long formula has no meaning, but conceptually the idea is the same.
Hypotheses
Ref Expression
wph
vx
Assertion
Ref Expression
wal

See definition df-ex 1542 for more information.

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