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

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

Proof of Theorem a9e
StepHypRef Expression
1 ax-i9 1439 1 𝑥 𝑥 = 𝑦
Colors of variables: wff set class
Syntax hints:  wex 1397
This theorem was proved from axioms:  ax-i9 1439
This theorem is referenced by:  ax9o  1604  equid  1605  equs4  1629  equsal  1631  equsex  1632  equsexd  1633  spimt  1640  spimeh  1643  spimed  1644  equvini  1657  ax11v2  1717  ax11v  1724  ax11ev  1725  equs5or  1727  euequ1  2011
  Copyright terms: Public domain W3C validator