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

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

Proof of Theorem a9e
StepHypRef Expression
1 ax-i9 1404 1 x x = y
Colors of variables: wff set class
Syntax hints:  wex 1362
This theorem was proved from axioms:  ax-i9 1404
This theorem is referenced by:  ax9o  1570  equid  1571  equs4  1595  equsal  1597  equsex  1598  equsexd  1599  spimt  1606  spimeh  1609  spimed  1610  equvini  1623  ax11v2  1683  ax11v  1690  ax11ev  1691  equs5or  1693  euequ1  1977
  Copyright terms: Public domain W3C validator