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

Theorem a9e 1586
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 1405 and ax-17 1419, all axioms other than ax-9 1424 are believed to be theorems of free logic, although the system without ax-9 1424 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
Ref Expression
a9e  |-  E. x  x  =  y

Proof of Theorem a9e
StepHypRef Expression
1 ax-i9 1423 1  |-  E. x  x  =  y
Colors of variables: wff set class
Syntax hints:   E.wex 1381
This theorem was proved from axioms:  ax-i9 1423
This theorem is referenced by:  ax9o  1588  equid  1589  equs4  1613  equsal  1615  equsex  1616  equsexd  1617  spimt  1624  spimeh  1627  spimed  1628  equvini  1641  ax11v2  1701  ax11v  1708  ax11ev  1709  equs5or  1711  euequ1  1995
  Copyright terms: Public domain W3C validator