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

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

Proof of Theorem a9e
StepHypRef Expression
1 ax-i9 1495 1 𝑥 𝑥 = 𝑦
Colors of variables: wff set class
Syntax hints:  wex 1453
This theorem was proved from axioms:  ax-i9 1495
This theorem is referenced by:  ax9o  1661  equid  1662  equs4  1688  equsal  1690  equsex  1691  equsexd  1692  spimt  1699  spimeh  1702  spimed  1703  equvini  1716  ax11v2  1776  ax11v  1783  ax11ev  1784  equs5or  1786  euequ1  2072
  Copyright terms: Public domain W3C validator