Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > a9e  Unicode version 
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 ax5 1267 through ax14 1338 and ax17 1350, all axioms other than ax9 1355 are believed to be theorems of free logic, although the system without ax9 1355 is probably not complete in free logic. (Contributed by NM, 5Aug1993.) (Revised by NM, 3Feb2015.) 
Ref  Expression 

a9e 
Step  Hyp  Ref  Expression 

1  axi9 1354  1 
Colors of variables: wff set class 
Syntax hints: wex 1313 
This theorem is referenced by: ax9o 1479 equid 1480 equs4 1503 equsex 1505 equsexd 1506 a4ime 1514 equvini 1525 ax11v2 1587 ax11v 1594 ax11ev 1595 equs5or 1597 pm11.07 1740 euequ1 2158 
This theorem was proved from axioms: axi9 1354 
Copyright terms: Public domain  W3C validator 