ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  a9e Unicode version

Theorem a9e 1556
Description: At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 1336 through ax-14 1396 and ax-17 1402, all axioms other than ax-9 1418 are believed to be theorems of free logic, although the system without ax-9 1418 is probably not complete in free logic.
Ref Expression

Proof of Theorem a9e
StepHypRef Expression
1 ax-i9 1417 1
Colors of variables: wff set class
Syntax hints:  wex 1374
This theorem is referenced by:  ax9o  1557  equid1  1561  equs4  1582  equsex  1584  a4ime  1593  equvini  1602  ax11v2  1651  pm11.07  1783  ax11eq  1810  ax11el  1811  ax11inda  1818  a12stdy1  1819  euequ1  1912
This theorem was proved from axioms:  ax-i9 1417
  Copyright terms: Public domain W3C validator