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

Theorem a9e 1674
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 1423 through ax-14 1492 and ax-17 1506, all axioms other than ax-9 1511 are believed to be theorems of free logic, although the system without ax-9 1511 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 1510 1 𝑥 𝑥 = 𝑦
Colors of variables: wff set class
Syntax hints:  wex 1468
This theorem was proved from axioms:  ax-i9 1510
This theorem is referenced by:  ax9o  1676  equid  1677  equs4  1703  equsal  1705  equsex  1706  equsexd  1707  spimt  1714  spimeh  1717  spimed  1718  equvini  1731  ax11v2  1792  ax11v  1799  ax11ev  1800  equs5or  1802  euequ1  2092
  Copyright terms: Public domain W3C validator