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

Theorem a9e 1478
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 1267 through ax-14 1338 and ax-17 1350, all axioms other than ax-9 1355 are believed to be theorems of free logic, although the system without ax-9 1355 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
Ref Expression

Proof of Theorem a9e
StepHypRef Expression
1 ax-i9 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:  ax-i9 1354
  Copyright terms: Public domain W3C validator